-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem sub_mul_div (x n p : Nat) (h₁ : n*p ≤ x) : (x - n*p) / n = x / n - p

Proof state:
case succ
x n : Nat
h₀ : n > 0
p : Nat
IH : n * p ≤ x → (x - n * p) / n = x / n - p
h₁ : n * (p + 1) ≤ x
h₂ : n * p ≤ x
h₃ : x - n * p ≥ n
⊢ (x - n * (p + 1)) / n = x / n - (p + 1)

Tactic:
rw [sub_succ, ← IH h₂, div_eq_sub_div h₀ h₃]

Result:
case succ
x n : Nat
h₀ : n > 0
p : Nat
IH : n * p ≤ x → (x - n * p) / n = x / n - p
h₁ : n * (p + 1) ≤ x
h₂ : n * p ≤ x
h₃ : x - n * p ≥ n
⊢ (x - n * (p + 1)) / n = ((x - n * p - n) / n + 1).pred

Proof state:
x n p : Nat
h₁ : n * p ≤ x
⊢ (x - n * p) / n = x / n - p

Tactic:
match eq_zero_or_pos n with
| .inl h₀ => rw [h₀, Nat.div_zero, Nat.div_zero, Nat.zero_sub]
| .inr h₀ => induction p with
  | zero => rw [Nat.mul_zero, Nat.sub_zero, Nat.sub_zero]
  | succ p IH =>
    have h₂ : n * p ≤ x := Nat.le_trans (Nat.mul_le_mul_left _ (le_succ _)) h₁
    have h₃ : x - n * p ≥ n := by
      apply Nat.le_of_add_le_add_right
      rw [Nat.sub_add_cancel h₂, Nat.add_comm]
      rw [mul_succ] at h₁
      exact h₁
    rw [sub_succ, ← IH h₂, div_eq_sub_div h₀ h₃]
    simp [Nat.pred_succ, mul_succ, Nat.sub_sub]

Result:
no goals

Proof state:
case succ
x n : Nat
h₀ : n > 0
p : Nat
IH : n * p ≤ x → (x - n * p) / n = x / n - p
h₁ : n * (p + 1) ≤ x
h₂ : n * p ≤ x
⊢ (x - n * (p + 1)) / n = x / n - (p + 1)

Tactic:
have h₃ : x - n * p ≥ n := by
  apply Nat.le_of_add_le_add_right
  rw [Nat.sub_add_cancel h₂, Nat.add_comm]
  rw [mul_succ] at h₁
  exact h₁

Result:
case succ
x n : Nat
h₀ : n > 0
p : Nat
IH : n * p ≤ x → (x - n * p) / n = x / n - p
h₁ : n * (p + 1) ≤ x
h₂ : n * p ≤ x
h₃ : x - n * p ≥ n
⊢ (x - n * (p + 1)) / n = x / n - (p + 1)

Proof state:
case succ
x n : Nat
h₀ : n > 0
p : Nat
IH : n * p ≤ x → (x - n * p) / n = x / n - p
h₁ : n * (p + 1) ≤ x
h₂ : n * p ≤ x
h₃ : x - n * p ≥ n
⊢ (x - n * (p + 1)) / n = ((x - n * p - n) / n + 1).pred

Tactic:
simp [Nat.pred_succ, mul_succ, Nat.sub_sub]

Result:
no goals

Proof state:
case a
x n : Nat
h₀ : n > 0
p : Nat
IH : n * p ≤ x → (x - n * p) / n = x / n - p
h₁ : n * (p + 1) ≤ x
h₂ : n * p ≤ x
⊢ n * p + n ≤ x

Tactic:
rw [mul_succ] at h₁

Result:
case a
x n : Nat
h₀ : n > 0
p : Nat
IH : n * p ≤ x → (x - n * p) / n = x / n - p
h₁ : n * p + n ≤ x
h₂ : n * p ≤ x
⊢ n * p + n ≤ x

Proof state:
case zero
x n : Nat
h₀ : n > 0
h₁ : n * 0 ≤ x
⊢ (x - n * 0) / n = x / n - 0

Tactic:
rw [Nat.mul_zero, Nat.sub_zero, Nat.sub_zero]

Result:
no goals

Proof state:
x n p : Nat
h₁ : n * p ≤ x
h₀ : n > 0
⊢ (x - n * p) / n = x / n - p

Tactic:
induction p with
| zero => rw [Nat.mul_zero, Nat.sub_zero, Nat.sub_zero]
| succ p IH =>
have h₂ : n * p ≤ x := Nat.le_trans (Nat.mul_le_mul_left _ (le_succ _)) h₁
have h₃ : x - n * p ≥ n := by
apply Nat.le_of_add_le_add_right
rw [Nat.sub_add_cancel h₂, Nat.add_comm]
rw [mul_succ] at h₁
exact h₁
rw [sub_succ, ← IH h₂, div_eq_sub_div h₀ h₃]
simp [Nat.pred_succ, mul_succ, Nat.sub_sub]

Result:
no goals

Proof state:
x n : Nat
h₀ : n > 0
p : Nat
IH : n * p ≤ x → (x - n * p) / n = x / n - p
h₁ : n * (p + 1) ≤ x
h₂ : n * p ≤ x
⊢ x - n * p ≥ n

Tactic:
apply Nat.le_of_add_le_add_right

Result:
case a
x n : Nat
h₀ : n > 0
p : Nat
IH : n * p ≤ x → (x - n * p) / n = x / n - p
h₁ : n * (p + 1) ≤ x
h₂ : n * p ≤ x
⊢ n + ?b ≤ x - n * p + ?b

case b
x n : Nat
h₀ : n > 0
p : Nat
IH : n * p ≤ x → (x - n * p) / n = x / n - p
h₁ : n * (p + 1) ≤ x
h₂ : n * p ≤ x
⊢ Nat

Proof state:
case a
x n : Nat
h₀ : n > 0
p : Nat
IH : n * p ≤ x → (x - n * p) / n = x / n - p
h₁ : n * (p + 1) ≤ x
h₂ : n * p ≤ x
⊢ n + ?b ≤ x - n * p + ?b

case b
x n : Nat
h₀ : n > 0
p : Nat
IH : n * p ≤ x → (x - n * p) / n = x / n - p
h₁ : n * (p + 1) ≤ x
h₂ : n * p ≤ x
⊢ Nat

Tactic:
rw [Nat.sub_add_cancel h₂, Nat.add_comm]

Result:
case a
x n : Nat
h₀ : n > 0
p : Nat
IH : n * p ≤ x → (x - n * p) / n = x / n - p
h₁ : n * (p + 1) ≤ x
h₂ : n * p ≤ x
⊢ n * p + n ≤ x

Proof state:
case a
x n : Nat
h₀ : n > 0
p : Nat
IH : n * p ≤ x → (x - n * p) / n = x / n - p
h₁ : n * p + n ≤ x
h₂ : n * p ≤ x
⊢ n * p + n ≤ x

Tactic:
exact h₁

Result:
no goals

Proof state:
x n p : Nat
h₁ : n * p ≤ x
h₀ : n = 0
⊢ (x - n * p) / n = x / n - p

Tactic:
rw [h₀, Nat.div_zero, Nat.div_zero, Nat.zero_sub]

Result:
no goals

Proof state:
case succ
x n : Nat
h₀ : n > 0
p : Nat
IH : n * p ≤ x → (x - n * p) / n = x / n - p
h₁ : n * (p + 1) ≤ x
⊢ (x - n * (p + 1)) / n = x / n - (p + 1)

Tactic:
have h₂ : n * p ≤ x := Nat.le_trans (Nat.mul_le_mul_left _ (le_succ _)) h₁

Result:
case succ
x n : Nat
h₀ : n > 0
p : Nat
IH : n * p ≤ x → (x - n * p) / n = x / n - p
h₁ : n * (p + 1) ≤ x
h₂ : n * p ≤ x
⊢ (x - n * (p + 1)) / n = x / n - (p + 1)