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

At: ndiff ndiff 1 1
1. a:
2. b:
3. c:

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

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

About:
intnatural_numberminusaddequal

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