int
2
Sections
StandardLIB
Doc
Theorem
Name
Thm*
a,b:
. (a -- b)+b = imax(a;b)
[ndiff_add_eq_imax]
cites
Thm*
a,b,c:
. imax(a;b)+c = imax(a+c;b+c)
[imax_add_r]
int
2
Sections
StandardLIB
Doc
a,b:
. (a -- b)+b = imax(a;b)a,b,c:. imax(a;b)+c = imax(a+c;b+c)a,b:. (a -- b)+b = imax(a;b)a,b,c:. imax(a;b)+c = imax(a+c;b+c)