IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
div inverts nat mul211 1. x : 2. y : 3. z:. x = yz (xz) = y 4. z : 5. x = yz 6. 0<y 7. 0<z (xz) = y
By:
BackThru: Hyp:3 ...
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
z:
z 
(x 
z) = y
(x 
