match z with
| 0 => rw [Nat.mul_zero, tsub_zero]
| Nat.succ z =>
  rewrite [Nat.mul_succ] at h
  have k : y * z ≤ x := Nat.le_trans (Nat.le_add_right _ _) h
  have l : y ≤ x - y * z := le_tsub_of_add_le_left h
  rewrite [Nat.mul_succ]
  rewrite [← tsub_tsub]
  rewrite [← Nat.mod_eq_sub_mod l]
  exact sub_mul_mod_self_left x y z k
x y z : ℕ
h : y * z ≤ x
⊢ (x - y * z) % y = x % y
no goals