(3steps total) PrintForm Definitions Lemmas SimpleMulFacts Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: div inverts nat mul2 1
1. x : 
2. y : 
3. z:. x = yz  (x  z) = y
4. z : 
5. x = yz
  (x  z) = y
By: Guarding (<prop> & <prop>)
FwdThru: Thm*  a,b:. 0<ab  0<a & 0<b on [ 0<yz ] ...

Generated subgoal:

1 6. 0<y
7. 0<z
  (x  z) = y
1 step

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

(3steps total) PrintForm Definitions Lemmas SimpleMulFacts Sections DiscrMathExt Doc