(7steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
int
seg
well
founded
down
1
1
1
1
1
1.
i:
2.
j:
{i...}
3.
WellFnd{u}({0...};x,y.x < y)
4.
WellFnd{u}({i..j
};x,y.-(j-y) < -(j-x))
WellFnd{u}({i..j
};x,y.x > y)
By:
RWH (LemmaWithC [`n',j]
Thm*
a,b,n:
. a < b
a+n < b+n) 4
THEN
ArithSimp 4
Generated subgoal:
1
4.
WellFnd{u}({i..j
};x,y.y < x)
WellFnd{u}({i..j
};x,y.x > y)
About:
(7steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
};x,y.y < x)
WellFnd{u}({i..j};x,y.x > y)
};x,y.-(j-y) < -(j-x)) WellFnd{u}({i..j};x,y.x > y)
a,b,n:. a < b 
a+n < b+n)
4
};x,y.y < x) WellFnd{u}({i..j};x,y.x > y)
