(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
x
:
,
y
,
z
:
.
x
=
y
z
(
x
z
) =
y
By:
SimilarTo
Thm*
x
,
y
:
,
z
:
.
x
=
y
z
(
x
z
) =
y
...
Generated subgoal:
1
1.
x
:
2.
y
:
3.
z
:
.
x
=
y
z
(
x
z
) =
y
4.
z
:
5.
x
=
y
z
(
x
z
) =
y
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
Definitions
Lemmas
SimpleMulFacts
Sections
DiscrMathExt
Doc
x:
, y,z:. x = y
z 
(x 
z) = y x:, y,z:. x = yz (x z) = yx,y:, z:. x = yz (x z) = y ...
z:. x = yz (x z) = y
z
(x z) = y
