Nuprl - Proof: minus imin

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: minus imin

a,b:

. -imin(a;b) = imax(-a;-b)

By:	Auto THEN Decide: ab THEN ElimImaxmin Auto 0

Generated subgoals:

1 1. a :
2. b :
3. ab
-a = -a
Auto

2 1. a :
2. b :
3. ab
-b = -b
Auto

About:

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

1	1. a : 2. b : 3. ab -a = -a	Auto
2	1. a : 2. b : 3. ab -b = -b	Auto