(22steps total)
PrintForm
Definitions
Lemmas
SimpleMulFacts
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
prime
nat
3
1
1
1.
x
:
2. 2
x
3.
(
i
:{2..
x
}.
i
|
x
)
(
x
~ 1)
By:
SimilarTo:
x
= 1 THEN BackThru:
Thm*
a
,
b
:
. (
a
~
b
)
a
=
b
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(22steps total)
PrintForm
Definitions
Lemmas
SimpleMulFacts
Sections
DiscrMathExt
Doc
x
(
i:{2..x
}. i | x)
(x ~ 1)
x
(i:{2..x}. i | x)
(x ~ 1)x = 1 THEN BackThru: Thm* 
a,b:. (a ~ b) 
a = b
