SimpleMulFacts
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
3
Thm*
y
:
. prime(-
y
)
prime(
y
)
[prime_neg]
cites the following:
2
Thm*
a
:
. (-
a
) ~
a
[neg_assoced]
0
Thm*
a
,
b
:
.
a
|
b
-
a
|
b
[divides_invar_1]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
SimpleMulFacts
Sections
DiscrMathExt
Doc
y:
. prime(-y) 
prime(y)a:. (-a) ~ aa,b:. a | b -a | by:. prime(-y) prime(y)a:. (-a) ~ aa,b:. a | b -a | b