Nuprl - Proof: quot rem exists n 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: quot rem exists n 1

1. a :

2. b :

, r:

b. a = q

b+r

By:	Assert (c:. (q:. a = qb+c) (q:, r:b. a = qb+r)) THENA Analyze 0

Generated subgoals:

1 3. c :
  (q:. a = qb+c)  (q:, r:b. a = qb+r)
5 steps

2 3. c:. (q:. a = qb+c)  (q:, r:b. a = qb+r)
  q:, r:b. a = qb+r
2 steps

About:

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

1	3. c : (q:. a = qb+c) (q:, r:b. a = qb+r)	5 steps
2	3. c:. (q:. a = qb+c) (q:, r:b. a = qb+r) q:, r:b. a = qb+r	2 steps