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

At: ndiff add eq imax

a,b:. (a -- b)+b = imax(a;b)
By:
UnivCD
THEN
Unfold `ndiff` 0
Generated subgoal:

11. a:
2. b:
imax(a-b;0)+b = imax(a;b)

About:
intnatural_numberaddsubtractequalall

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