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

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

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

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

About:
intnatural_numberminusaddequal

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