Nuprl - Proof: mul preserves le 1 1

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

1. a :

2. b :

3. n :

4. 0<n
5. a

(n-1)

b
6. a

By:

Analyze5

Generated subgoal:

1 5. ab
6. (n-1)a(n-1)b
nanb
Auto

About:

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