Documentation
Time
.
Data
.
Int
.
Order
Search
return to top
source
Imports
Init
Init.Data.Int.Order
Imported by
Int
.
lt_of_ediv_eq
source
theorem
Int
.
lt_of_ediv_eq
{
a
b
:
Int
}
{
n
:
Nat
}
(
hb
:
0
<
b
)
(
h
:
a
/
b
=
↑
n
)
:
a
<
b
+
↑
n
*
b