num
thy
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
2
Thm*
a
,
b
:
. gcd(
a
;
b
)
[gcd_wf]
cites the following:
1
Thm*
a
:
,
n
:
. |
a
rem
n
|<|
n
|
[rem_mag_bound]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
num
thy
1
Sections
StandardLIB
Doc
a,b:
. gcd(a;b) 
a:, n:
. |a rem n|<|n|a,b:. gcd(a;b) a:, n:. |a rem n|<|n|