(3steps total)
PrintForm
Definitions
Lemmas
FTA
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
factor
divides
evalfactorization
a
,
b
:
,
f
:({
a
..
b
}
),
j
:{
a
..
b
}. 0<
f
(
j
)
j
|
{
a
..
b
}(
f
)
By:
Auto
Generated subgoal:
1
1.
a
:
2.
b
:
3.
f
: {
a
..
b
}
4.
j
: {
a
..
b
}
5. 0<
f
(
j
)
j
|
{
a
..
b
}(
f
)
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
Definitions
Lemmas
FTA
Sections
DiscrMathExt
Doc
a,b:
, f:({a..b
}
), j:{a..b
j | 
{a..b
