 Timestamp:
 Oct 10, 2011, 4:03:19 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/extralib.ma
r1316 r1337 121 121 lemma Zmax_l: ∀x,y. x ≤ Zmax x y. 122 122 #x #y whd in ⊢ (??%) lapply (Z_compare_to_Prop x y) cases (Z_compare x y) 123 /3/ whd in ⊢ (% → ??%) /3/qed.123 /3/ qed. 124 124 125 125 lemma Zmax_r: ∀x,y. y ≤ Zmax x y.
Note: See TracChangeset
for help on using the changeset viewer.