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

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

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

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

About:
intnatural_numberminusaddequal

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