Basic lemmas about division and modulo for integers

emod

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

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