Nuprl - Proof: mul preserves le 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: mul preserves le 1

1. a :

2. b :

. a

By:	NatInd Concl

Generated subgoal:

1 3. n :
4. 0<n
5. ab (n-1)a(n-1)b
6. ab
nanb
2 steps

About:

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