LeanPool.EcTateLean.Init.Data.Int.Lemmas

Imported Lean Pool material for LeanPool.EcTateLean.Init.Data.Int.Lemmas.

theorem mod_neg_right (m k : ℤ) : m % -k = m % k

theorem div_neg_right (m k : ℤ) : m / -k = -(m / k)

@[simp]

theorem Int.ofNat_zero_eq_zero : ofNat Nat.zero = 0