Documentation

Time.Data.Int.Order

theorem Int.lt_of_ediv_eq {a b : Int} {n : Nat} (hb : 0 < b) (h : a / b = n) :
a < b + n * b