(8steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
ndiff
ndiff
a,b:
, c:
. ((a -- b) -- c) = (a -- (b+c))
By:
UnivCD
THEN
Unfold `ndiff` 0
Generated subgoal:
1
1.
a:
2.
b:
3.
c:
imax(imax(a-b;0)-c;0) = imax(a-(b+c);0)
About:
(8steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
imax(imax(a-b;0)-c;0) = imax(a-(b+c);0) 
a,b:, c:. ((a -- b) -- c) = (a -- (b+c)) imax(imax(a-b;0)-c;0) = imax(a-(b+c);0)
