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

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

imax(b;0) = b
By:
Unfold `imax` 0
THEN
SplitOnConclITE
Generated subgoals:

None

About:
intnatural_numberless_thanequal

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