Basic lemmas about division and modulo for integers

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.emod_eq_sub_self_emod {a b : Int} : a % b = (a - b) % b