Basic lemmas about division and modulo for integers

theorem Int.natCast_emod (m n : Nat) : ↑(m % n) = ↑m % ↑n

theorem Int.add_emod_right {a b : Int} : (a + b) % b = a % b

theorem Int.add_emod_left {a b : Int} : (a + b) % a = b % a

ediv and fdiv

theorem Int.mul_ediv_le_mul_ediv_assoc {a : Int} (ha : 0 ≤ a) (b : Int) {c : Int} (hc : 0 ≤ c) : a * (b / c) ≤ a * b / c

theorem Int.ediv_ediv_eq_ediv_mul (m : Int) {n k : Int} (hn : 0 ≤ n) : m / n / k = m / (n * k)

theorem Int.fdiv_fdiv_eq_fdiv_mul (m : Int) {n k : Int} (hn : 0 ≤ n) (hk : 0 ≤ k) : (m.fdiv n).fdiv k = m.fdiv (n * k)

emod

theorem Int.sub_emod_right (a b : Int) : (a - b) % b = a % b

theorem Int.emod_eq_sub_self_emod {a b : Int} : a % b = (a - b) % b