PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
division3
sfa
k
:
,
r1
,
r2
:
k
,
q1
,
q2
:
.
q1
k
-
r1
= -(
q2
k
+
r2
)
q1
= -
q2
&
r1
=
r2
By:
UnivCD
THEN
FwdThru:
Thm*
k
:
,
r1
,
r2
:
k
,
q1
,
q2
:
.
q1
k
+
r1
=
q2
k
+
r2
q1
=
q2
&
r1
=
r2
on [ (-
q1
)
k
+
r1
=
q2
k
+
r2
]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc