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