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

At: imin add r

a,b,c:. imin(a;b)+c = imin(a+c;b+c)
By:
UnivCD
THEN
BackThru Thm* i,j:. i = j -i = -j
THEN
ArithSimp 0
Generated subgoal:

11. a:
2. b:
3. c:
-c+-imin(a;b) = -imin(a+c;b+c)

About:
intminusaddequalall

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