no goals
x n p : Nat
h₁ : n * p ≤ x
⊢ (x - n * p) / n = x / n - p
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 [add_one, Nat.pred_succ, mul_succ, Nat.sub_sub]
no goals
x n p : Nat
h₁ : n * p ≤ x
h₀ : n = 0
⊢ (x - n * p) / n = x / n - p
rw [h₀, Nat.div_zero, Nat.div_zero, Nat.zero_sub]
no goals
x n p : Nat
h₁ : n * p ≤ x
h₀ : n > 0
⊢ (x - n * p) / n = x / n - p
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 [add_one, Nat.pred_succ, mul_succ, Nat.sub_sub]
no goals
case zero
x n : Nat
h₀ : n > 0
h₁ : n * zero ≤ x
⊢ (x - n * zero) / n = x / n - zero
rw [Nat.mul_zero, Nat.sub_zero, Nat.sub_zero]
case succ
x n : Nat
h₀ : n > 0
p : Nat
IH : n * p ≤ x → (x - n * p) / n = x / n - p
h₁ : n * succ p ≤ x
h₂ : n * p ≤ x
⊢ (x - n * succ p) / n = x / n - succ p
case succ
x n : Nat
h₀ : n > 0
p : Nat
IH : n * p ≤ x → (x - n * p) / n = x / n - p
h₁ : n * succ p ≤ x
⊢ (x - n * succ p) / n = x / n - succ p
have h₂ : n * p ≤ x := Nat.le_trans (Nat.mul_le_mul_left _ (le_succ _)) h₁
case succ
x n : Nat
h₀ : n > 0
p : Nat
IH : n * p ≤ x → (x - n * p) / n = x / n - p
h₁ : n * succ p ≤ x
h₂ : n * p ≤ x
h₃ : x - n * p ≥ n
⊢ (x - n * succ p) / n = x / n - succ p
case succ
x n : Nat
h₀ : n > 0
p : Nat
IH : n * p ≤ x → (x - n * p) / n = x / n - p
h₁ : n * succ p ≤ x
h₂ : n * p ≤ x
⊢ (x - n * succ p) / n = x / n - succ p
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₁
case succ
x n : Nat
h₀ : n > 0
p : Nat
IH : n * p ≤ x → (x - n * p) / n = x / n - p
h₁ : n * succ p ≤ x
h₂ : n * p ≤ x
h₃ : x - n * p ≥ n
⊢ (x - n * succ p) / n = pred ((x - n * p - n) / n + 1)
case succ
x n : Nat
h₀ : n > 0
p : Nat
IH : n * p ≤ x → (x - n * p) / n = x / n - p
h₁ : n * succ p ≤ x
h₂ : n * p ≤ x
h₃ : x - n * p ≥ n
⊢ (x - n * succ p) / n = x / n - succ p
rw [sub_succ, ← IH h₂, div_eq_sub_div h₀ h₃]
no goals
case succ
x n : Nat
h₀ : n > 0
p : Nat
IH : n * p ≤ x → (x - n * p) / n = x / n - p
h₁ : n * succ p ≤ x
h₂ : n * p ≤ x
h₃ : x - n * p ≥ n
⊢ (x - n * succ p) / n = pred ((x - n * p - n) / n + 1)
simp [add_one, Nat.pred_succ, mul_succ, Nat.sub_sub]
case a
x n : Nat
h₀ : n > 0
p : Nat
IH : n * p ≤ x → (x - n * p) / n = x / n - p
h₁ : n * succ p ≤ 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 * succ p ≤ x
h₂ : n * p ≤ x
⊢ Nat
x n : Nat
h₀ : n > 0
p : Nat
IH : n * p ≤ x → (x - n * p) / n = x / n - p
h₁ : n * succ p ≤ x
h₂ : n * p ≤ x
⊢ x - n * p ≥ n
apply Nat.le_of_add_le_add_right
case a
x n : Nat
h₀ : n > 0
p : Nat
IH : n * p ≤ x → (x - n * p) / n = x / n - p
h₁ : n * succ p ≤ x
h₂ : n * p ≤ x
⊢ n * p + n ≤ x
case a
x n : Nat
h₀ : n > 0
p : Nat
IH : n * p ≤ x → (x - n * p) / n = x / n - p
h₁ : n * succ p ≤ 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 * succ p ≤ x
h₂ : n * p ≤ x
⊢ Nat
rw [Nat.sub_add_cancel h₂, Nat.add_comm]
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
case a
x n : Nat
h₀ : n > 0
p : Nat
IH : n * p ≤ x → (x - n * p) / n = x / n - p
h₁ : n * succ p ≤ x
h₂ : n * p ≤ x
⊢ n * p + n ≤ x
rw [mul_succ] at h₁
no goals
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
exact h₁