Changeset 961 for src/utilities/extranat.ma
- Timestamp:
- Jun 15, 2011, 4:15:52 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/utilities/extranat.ma
r744 r961 19 19 ] 20 20 ]. 21 22 lemma nat_compare_eq : ∀n. nat_compare n n = nat_eq n. 23 #n elim n 24 [ @refl 25 | #m #IH whd in ⊢ (??%?) > IH @refl 26 ] qed. 27 28 lemma nat_compare_lt : ∀n,m. nat_compare n (n+S m) = nat_lt n m. 29 #n #m elim n 30 [ // 31 | #n' #IH whd in ⊢ (??%?) > IH @refl 32 ] qed. 33 34 lemma nat_compare_gt : ∀n,m. nat_compare (m+S n) m = nat_gt n m. 35 #n #m elim m 36 [ // 37 | #m' #IH whd in ⊢ (??%?) > IH @refl 38 ] qed. 21 39 22 40 lemma max_l : ∀m,n,o:nat. o ≤ m → o ≤ max m n.
Note: See TracChangeset
for help on using the changeset viewer.