(3steps total)
PrintForm
Definitions
Lemmas
num
thy
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
gcd
mul
1
1.
a
:
2.
b
:
3.
n
:
(
n
gcd(
a
;
b
)) ~ gcd(
n
a
;
n
b
)
By:
(FunElim (gcd(
a
;
b
) =
y
)) THEN (FunElim (gcd(
n
a
;
n
b
) =
z
))
Generated subgoal:
1
4.
y
:
5. GCD(
a
;
b
;
y
)
6.
z
:
7. GCD(
n
a
;
n
b
;
z
)
(
n
y
) ~
z
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
Definitions
Lemmas
num
thy
1
Sections
StandardLIB
Doc
(n
gcd(a;b)) ~ gcd(na;nb)
(ngcd(a;b)) ~ gcd(na;nb)a;nb) = z))
a;nb;z)
(ny) ~ z
