Ignore:
Timestamp:
Dec 7, 2011, 3:48:32 PM (8 years ago)
Author:
boender
Message:
  • cleaned up Assembly, moved some definitions elsewhere
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/extranat.ma

    r1516 r1593  
    6363] qed.
    6464
     65lemma le_S_to_le: ∀n,m:ℕ.S n ≤ m → n ≤ m.
     66 /2/ qed.
     67
     68lemma le_plus_k:
     69  ∀n,m:ℕ.n ≤ m → ∃k:ℕ.m = n + k.
     70 #n #m elim m -m;
     71 [ #Hn % [ @O | <(le_n_O_to_eq n Hn) // ]
     72 | #m #Hind #Hn cases (le_to_or_lt_eq … Hn) -Hn; #Hn
     73   [ elim (Hind (le_S_S_to_le … Hn)) #k #Hk % [ @(S k) | >Hk // ]
     74   | % [ @O | <Hn // ]
     75   ]
     76 ]
     77qed.
     78
     79lemma eq_plus_S_to_lt:
     80  ∀n,m,p:ℕ.n = m + (S p) → m < n.
     81 #n #m #p /2 by lt_plus_to_lt_l/
     82qed.
    6583
    6684(* "Fast" proofs:  some proofs get reduced during normalization (in particular,
Note: See TracChangeset for help on using the changeset viewer.