Nuprl - Proof: rem gen base case 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: rem gen base case 1

1. a :

2. n :

3. |a|<|n|

(a rem n) = a

By:	Decide: 0a THEN ElimAbsVal Auto Hyp:3

Generated subgoals:

1 3. a<n
4. 0a
(a rem n) = a
1 step

2 3. -a<n
4. 0a
(a rem n) = a
2 steps

About:

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

1	3. a<n 4. 0a (a rem n) = a	1 step
2	3. -a<n 4. 0a (a rem n) = a	2 steps