no goals
x y z : Nat
⊢ (x + y * z) % y = x % y
match z with
| 0 => rw [Nat.mul_zero, Nat.add_zero]
| succ z => rw [mul_succ, ← Nat.add_assoc, add_mod_right, add_mul_mod_self_left (z := z)]
no goals
x y z : Nat
⊢ (x + y * 0) % y = x % y
rw [Nat.mul_zero, Nat.add_zero]
no goals
x y z✝ z : Nat
⊢ (x + y * succ z) % y = x % y
rw [mul_succ, ← Nat.add_assoc, add_mod_right, add_mul_mod_self_left (z := z)]