theorem Int.toNat_lt_toNat {a : Int} {b : Int} (h : a < b) (hb : 0 < b) : a.toNat < b.toNat

theorem Int.lt_toNat {n : Nat} {a : Int} (h : ↑n < a) (hb : 0 < a) : n < a.toNat

theorem Int.toNat_le_toNat {a : Int} {b : Int} (h : a ≤ b) : a.toNat ≤ b.toNat

theorem Int.toNat_le {a : Int} {n : Nat} (h : a ≤ ↑n) : a.toNat ≤ n

theorem Int.le_of_eq {n : Int} {m : Int} (h : n = m) : n ≤ m

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