(3steps total)
PrintForm
Definitions
Lemmas
SimpleMulFacts
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
no
nat
prime
divs
one
1
1.
b
:
2.
b
| 1
3.
b
= 1
prime(
b
)
By:
Rewrite by
b
= 1
THEN
Rewrite by
Thm*
x
:
. prime(
x
)
2
x
&
(
i
:{2..
x
}.
i
|
x
)
Generated subgoal:
1
(2
1 &
(
i
:{2..1
}.
i
| 1))
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
Definitions
Lemmas
SimpleMulFacts
Sections
DiscrMathExt
Doc
prime(b)
prime(b)
x:. prime(x) 
2
x & (
i:{2..x
}. i | x) (21 & (i:{2..1}. i | 1))
