Changeset 1628 for src/utilities/binary/positive.ma
 Timestamp:
 Dec 19, 2011, 2:48:35 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/binary/positive.ma
r1587 r1628 1161 1161 λn,m. match leb n m with [ true ⇒ m  _ ⇒ n]. 1162 1162 1163 lemma commutative_max : commutative Pos max. 1164 #n #m whd in ⊢ (??%%); 1165 lapply (pos_compare_to_Prop n m) 1166 cases (pos_compare n m) whd in ⊢ (% → ?); #H 1167 [ >(le_to_leb_true n m) >(not_le_to_leb_false m n) /2/ 1168  >H @refl 1169  >(le_to_leb_true m n) >(not_le_to_leb_false n m) /2/ 1170 ] qed. 1171 1172 lemma max_l : ∀m,n:Pos. m ≤ max m n. 1173 #m #n normalize @leb_elim // 1174 qed. 1175 1176 lemma max_r : ∀m,n:Pos. n ≤ max m n. 1177 #m #n >commutative_max // 1178 qed. 1163 1179 1164 1180
Note: See TracChangeset
for help on using the changeset viewer.