Changeset 1338


Ignore:
Timestamp:
Oct 10, 2011, 4:05:50 PM (8 years ago)
Author:
sacerdot
Message:

Automation is now stronger.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/extralib.ma

    r1337 r1338  
    567567          normalize in ⊢ (?(???%)?); % /2/; @plt_pos
    568568          [ 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/; ]]]]
     570qed.
    576571
    577572lemma mod0_divides: ∀m,n,dv:Pos.
Note: See TracChangeset for help on using the changeset viewer.