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

At: ndiff ndiff eq imin 1 1
1. a:
2. b:

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

1 imax(imin(b;a);0) = imin(a;b)

About:
intnatural_numberminusaddequal

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