Changeset 1338 for src/utilities
 Timestamp:
 Oct 10, 2011, 4:05:50 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/extralib.ma
r1337 r1338 567 567 normalize in ⊢ (?(???%)?); % /2/; @plt_pos 568 568 [ cut (succ n' + r'' < p0 (succ n')); /2/; 569  cut (succ n' + r'' < p0 (succ n')); /2/; 570  /2/; 571  /2/; 572 ] 573 ] 574 ] 575 ] qed. 569  cut (succ n' + r'' < p0 (succ n')); /2/; ]]]] 570 qed. 576 571 577 572 lemma mod0_divides: ∀m,n,dv:Pos.
Note: See TracChangeset
for help on using the changeset viewer.