Nuprl - Proof: mul preserves lt 1

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

1. a :

2. b :

3. n :

4. a<b

a<n

By:	Inst: Thm* a,b:, n:. ab nanb Using:[a \| b-1 \| n]

Generated subgoal:

1 5. nan(b-1)
na<nb
Auto

About:

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