Changeset 2149 for src/ASM/Util.ma


Ignore:
Timestamp:
Jul 3, 2012, 4:19:38 AM (7 years ago)
Author:
sacerdot
Message:

Code shuffling to proper places.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r2125 r2149  
    17251725qed.
    17261726
     1727lemma flatten_singleton:
     1728 ∀A,a. flatten A [a] = a.
     1729#A #a normalize //
     1730qed.
     1731
     1732lemma length_flatten_cons:
     1733 ∀A,hd,tl.
     1734  |flatten A (hd::tl)| = |hd| + |flatten A tl|.
     1735 #A #hd #tl normalize //
     1736qed.
     1737
     1738lemma tech_transitive_lt_3:
     1739 ∀n1,n2,n3,b.
     1740  n1 < b → n2 < b → n3 < b →
     1741   n1 + n2 + n3 < 3 * b.
     1742 #n1 #n2 #n3 #b #H1 #H2 #H3
     1743 @(transitive_lt … (b + n2 + n3)) [ @monotonic_lt_plus_l @monotonic_lt_plus_l // ]
     1744 @(transitive_lt … (b + b + n3)) [ @monotonic_lt_plus_l @monotonic_lt_plus_r // ]
     1745 @(lt_to_le_to_lt … (b + b + b)) [ @monotonic_lt_plus_r // ] //
     1746qed.
     1747
     1748lemma m_lt_1_to_m_refl_0:
     1749  ∀m: nat.
     1750    m < 1 → m = 0.
     1751  #m cases m try (#irrelevant %)
     1752  #m' whd in ⊢ (% → ?); #relevant
     1753  lapply (le_S_S_to_le … relevant)
     1754  change with (? < ? → ?) -relevant #relevant
     1755  cases (lt_to_not_zero … relevant)
     1756qed.
Note: See TracChangeset for help on using the changeset viewer.