no goals
x k n : Nat
h₁ : n * k ≤ x
⊢ (x - n * k) % n = x % n
match k with
| 0 => rw [Nat.mul_zero, Nat.sub_zero]
| succ k =>
  have h₂ : n * k ≤ x := Nat.le_trans (le_add_right _ n) h₁
  have h₄ : x - n * k ≥ n := by
    apply Nat.le_of_add_le_add_right (b := n * k)
    rw [Nat.sub_add_cancel h₂]
    simp [mul_succ, Nat.add_comm] at h₁; simp [h₁]
  rw [mul_succ, ← Nat.sub_sub, ← mod_eq_sub_mod h₄, sub_mul_mod h₂]
no goals
x k n : Nat
h₁ : n * 0 ≤ x
⊢ (x - n * 0) % n = x % n
rw [Nat.mul_zero, Nat.sub_zero]
x k✝ n k : Nat
h₁ : n * succ k ≤ x
h₂ : n * k ≤ x
⊢ (x - n * succ k) % n = x % n
x k✝ n k : Nat
h₁ : n * succ k ≤ x
⊢ (x - n * succ k) % n = x % n
have h₂ : n * k ≤ x := Nat.le_trans (le_add_right _ n) h₁
x k✝ n k : Nat
h₁ : n * succ k ≤ x
h₂ : n * k ≤ x
h₄ : x - n * k ≥ n
⊢ (x - n * succ k) % n = x % n
x k✝ n k : Nat
h₁ : n * succ k ≤ x
h₂ : n * k ≤ x
⊢ (x - n * succ k) % n = x % n
have h₄ : x - n * k ≥ n := by
  apply Nat.le_of_add_le_add_right (b := n * k)
  rw [Nat.sub_add_cancel h₂]
  simp [mul_succ, Nat.add_comm] at h₁; simp [h₁]
no goals
x k✝ n k : Nat
h₁ : n * succ k ≤ x
h₂ : n * k ≤ x
h₄ : x - n * k ≥ n
⊢ (x - n * succ k) % n = x % n
rw [mul_succ, ← Nat.sub_sub, ← mod_eq_sub_mod h₄, sub_mul_mod h₂]
x k✝ n k : Nat
h₁ : n * succ k ≤ x
h₂ : n * k ≤ x
⊢ n + n * k ≤ x - n * k + n * k
x k✝ n k : Nat
h₁ : n * succ k ≤ x
h₂ : n * k ≤ x
⊢ x - n * k ≥ n
apply Nat.le_of_add_le_add_right (b := n * k)
x k✝ n k : Nat
h₁ : n * succ k ≤ x
h₂ : n * k ≤ x
⊢ n + n * k ≤ x
x k✝ n k : Nat
h₁ : n * succ k ≤ x
h₂ : n * k ≤ x
⊢ n + n * k ≤ x - n * k + n * k
rw [Nat.sub_add_cancel h₂]
x k✝ n k : Nat
h₂ : n * k ≤ x
h₁ : n + n * k ≤ x
⊢ n + n * k ≤ x
x k✝ n k : Nat
h₁ : n * succ k ≤ x
h₂ : n * k ≤ x
⊢ n + n * k ≤ x
simp [mul_succ, Nat.add_comm] at h₁
no goals
x k✝ n k : Nat
h₂ : n * k ≤ x
h₁ : n + n * k ≤ x
⊢ n + n * k ≤ x
simp [h₁]