IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
prime factorization exists112 1. n : {1...}
2. n = 1
g:({2..(n+1)}). n = {2..n+1}(g)
By:
{just factor n as itself }
Witness: trivial_factorization(n) ... THEN
BackThru: Thm*a,b:, j:{a..b}. {a..b}(trivial_factorization(j)) = j ...w
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
n = 1
g:({2..(n+1)
}
). n = 
{2..n+1
a,b:
, j:{a..b
