Changeset 1593 for src/utilities/extranat.ma
 Timestamp:
 Dec 7, 2011, 3:48:32 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/extranat.ma
r1516 r1593 63 63 ] qed. 64 64 65 lemma le_S_to_le: ∀n,m:ℕ.S n ≤ m → n ≤ m. 66 /2/ qed. 67 68 lemma 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 ] 77 qed. 78 79 lemma 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/ 82 qed. 65 83 66 84 (* "Fast" proofs: some proofs get reduced during normalization (in particular,
Note: See TracChangeset
for help on using the changeset viewer.