Nuprl - Proof: div inverts nat mul

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: div inverts nat mul

x,y:

, z:

. x = y

z) = y

By:

Auto

Generated subgoal:

1 1. x :
2. y :
3. z :
4. x = yz
(x z) = y
4 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html