Nuprl - Proof: mul cancel in lt 1 1

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

1. a :

2. b :

3. n :

4. n

a<n

b
5.

a<b

By:	Inst Thm* a,b:, n:. ab nanb [b;a;n]

Generated subgoals:

None

About:

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