Changeset 1515 for src/utilities/extralib.ma
 Timestamp:
 Nov 18, 2011, 1:03:14 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/extralib.ma
r1350 r1515 389 389 definition mod ≝ λm,n. snd ?? (divide m n). 390 390 391 lemma pred_minus: ∀n,m . pred n  m = pred (nm).391 lemma pred_minus: ∀n,m:Pos. pred n  m = pred (nm). 392 392 @pos_elim /3/; 393 393 qed.
Note: See TracChangeset
for help on using the changeset viewer.