int
2
Sections
StandardLIB
Doc
Rank
Theorem
Name
4
Thm*
n:
. WellFnd{i}({...n};x,y.x > y)
[int_lower_well_founded]
cites
2
Thm*
WellFnd{i}(
;x,y.x < y)
[nat_well_founded]
1
Thm*
r:(A
A
Prop), B:Type, f:(B
A). WellFnd{i}(A;x,y.r(x,y))
WellFnd{i}(B;x,y.r(f(x),f(y)))
[inv_image_ind]
3
Thm*
a,b,n:
. a < b
a+n < b+n
[add_mono_wrt_lt]
0
Thm*
i,j:
. i > j
-i < -j
[minus_mono_wrt_lt]
int
2
Sections
StandardLIB
Doc