rewrite [Nat.mul_succ]
x y z✝ z : ℕ
h : y * z + y ≤ x
k : y * z ≤ x
l : y ≤ x - y * z
⊢ (x - y * Nat.succ z) % y = x % y
x y z✝ z : ℕ
h : y * z + y ≤ x
k : y * z ≤ x
l : y ≤ x - y * z
⊢ (x - (y * z + y)) % y = x % y