no goals
a b c : Int
cz : c = 0
⊢ (a + b * c) % c = a % c
rw [cz, Int.mul_zero, Int.add_zero]
no goals
a b c : Int
cz : ¬c = 0
⊢ (a + b * c) % c = a % c
rw [Int.emod_def, Int.emod_def, Int.add_mul_ediv_right _ _ cz, Int.add_comm _ b,
  Int.mul_add, Int.mul_comm, ← Int.sub_sub, Int.add_sub_cancel]