(3steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc

At: imin add r 1
1. a:
2. b:
3. c:

-c+-imin(a;b) = -imin(a+c;b+c)
By:
RWH (LemmaC Thm* a,b:. -imin(a;b) = imax(-a;-b)) 0
THEN
RWN 1 (LemmaC Thm* a,b:. a+b = b+a) 0
Generated subgoal:

1 imax(-a;-b)+-c = imax(-(a+c);-(b+c))

About:
intminusaddequal

(3steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc