Nuprl - Proof: factorial ratio2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: factorial ratio2 1

1. m :

2. k :

3. m

k
4. k! = (k-m)!

k!m

k!m = ((k!)

((k-m)!))

By:	ElaborateDivision Auto Concl

Generated subgoal:

1 5. k! = ((k!)  ((k-m)!))(k-m)!+((k!) rem (k-m)!)
6. ((k!) rem (k-m)!)  ((k-m)!)
  k!m = ((k!)  ((k-m)!))
1 step

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html