num
thy
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
a
,
b
:
. CoPrime(
a
,
b
)
(gcd(
a
;
b
) ~ 1)
[coprime_elim_a]
cites the following:
Thm*
a
,
b
,
y1
,
y2
:
. GCD(
a
;
b
;
y1
)
GCD(
a
;
b
;
y2
)
(
y1
~
y2
)
[gcd_unique]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
num
thy
1
Sections
StandardLIB
Doc
a,b:
. CoPrime(a,b) 
(gcd(a;b) ~ 1)a,b,y1,y2:. GCD(a;b;y1) 
GCD(a;b;y2) (y1 ~ y2)a,b:. CoPrime(a,b) (gcd(a;b) ~ 1)a,b,y1,y2:. GCD(a;b;y1) GCD(a;b;y2) (y1 ~ y2)