1. m : 
2. k : 
3. mk
4. k! = (k-m)!k!m
5. k! = ((k!)  ((k-m)!))(k-m)!+((k!) rem (k-m)!)
6. ((k!) rem (k-m)!)  ((k-m)!)
  k!m = ((k!)  ((k-m)!))

By:	Inst: Thm*  k:, q1,q2:, r1,r2:k. q1k+r1 = q2k+r2  q1 = q2 & r1 = r2 Using:[(k-m)! | k!m | (k!)  ((k-m)!) | 0 | (k!) rem (k-m)!]

None

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