Problem
Theorem: For integers a and b and natural number c, (a -- b) -- c = a -- (b + c).
Consider that a and b are integers and c is a natural number. Now, the original expression can be transformed to imax(imax(a - b;0) - c;0) = imax(a - (b + c);0). From the add_com lemma, we conclude imax(-c + imax(a + -b;0);0) = imax(a + -b + -c;0). From the imax_assoc lemma, the goal becomes imax(imax((a + -b) + -c;0 + -c);0) = imax(a + -b + -c;0). There are 2 possible cases. The case 0 + -c <= 0 is trivial. Consider 0 < 0 + -c. Now, the original expression can be transformed to imax((a + -b) + -c;0 + -c) = imax(a + -b + -c;0). Equivalently, the original expression can be rewritten as
imax((a + -b) + -c) = imax(a + -b + -c;0). This proves the theorem.
"a,b:N. "c:Z. (a -- b) -- c = a -- (b + c)
BY (UnivCD ...a) THEN Unfold `ndiff` 0
imax(imax(a - b;0) - c;0) = imax(a - (b + c);0)
imax(-c + imax(a + -b;0);0) = imax(a + -b + -c;0)
BY RWN 1 (LemmaC `add_com`) 0
| THENM RWH (LemmaC `imax_add_r`) 0 THENA Auto
imax(imax((a + -b) + -c;0 + -c);0) = imax(a + -b + -c;0)
BY RWH (RevLemmaC `imax_assoc`) 0 THENA Auto
imax((a + -b) + -c;imax(0 + -c;0)) = imax(a + -b + -c;0)
BY RWN 2 (UnfoldTopC `imax`) 0
| THEN SplitOnConclITE THENA Auto'
| imax((a + -b) + -c;0) = imax(a + -b + -c;0)