Further lemmas about Int relying on omega automation.

@[simp]

theorem Int.toNat_sub' (a : Int) (b : Nat) : (a - ↑b).toNat = a.toNat - b

@[simp]

theorem Int.toNat_sub_max_self (a : Int) : (a - max a 0).toNat = 0

@[simp]

theorem Int.toNat_sub_self_max (a : Int) : (a - max 0 a).toNat = 0

theorem Int.bmod_neg_iff {m : Nat} {x : Int} (h2 : -↑m ≤ x) (h1 : x < ↑m) : x.bmod m < 0 ↔ -(↑m / 2) ≤ x ∧ x < 0 ∨ (↑m + 1) / 2 ≤ x

@[simp]

theorem Int.natCast_le_zero {n : Nat} : ↑n ≤ 0 ↔ n = 0

@[simp]

theorem Int.toNat_eq_zero {n : Int} : n.toNat = 0 ↔ n ≤ 0

theorem Int.eq_zero_of_dvd_of_natAbs_lt_natAbs {d n : Int} (h : d ∣ n) (h₁ : n.natAbs < d.natAbs) : n = 0

theorem Int.bmod_eq_self_of_le {n : Int} {m : Nat} (hn' : -(↑m / 2) ≤ n) (hn : n < (↑m + 1) / 2) : n.bmod m = n