Changeset 2670 for src/utilities
 Timestamp:
 Feb 15, 2013, 11:27:59 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/extranat.ma
r2286 r2670 61 61 [ @H 62 62  @(transitive_le … H) @(transitive_le … (not_le_to_lt … H')) // 63 ] qed. 64 65 lemma max_O_n : ∀n. max O n = n. 66 * // 67 qed. 68 69 lemma max_n_O : ∀n. max n O = n. 70 * // 71 qed. 72 73 lemma associative_max : associative nat max. 74 #n #m #o normalize 75 @(leb_elim n m) 76 [ normalize @(leb_elim m o) normalize #H1 #H2 77 [ >(le_to_leb_true n o) /2/ 78  >(le_to_leb_true n m) // 79 ] 80  normalize @(leb_elim m o) normalize #H1 #H2 81 [ % 82  >(not_le_to_leb_false … H2) 83 >(not_le_to_leb_false n o) // @lt_to_not_le @(transitive_lt … m) /2/ 84 ] 63 85 ] qed. 64 86
Note: See TracChangeset
for help on using the changeset viewer.