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

At: int lower well founded 1 1 1 1 1
1. n:
2. WellFnd{i}(;x,y.x < y)
3. WellFnd{i}({...n};x,y.-(n-y)+n < -(n-x)+n)

WellFnd{i}({...n};x,y.x > y)
By: ArithSimp 3
Generated subgoal:

13. WellFnd{i}({...n};x,y.y < x)
WellFnd{i}({...n};x,y.x > y)

About:
intminusaddsubtractless_than

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