no goals
a✝ b m n k a : ℕ
⊢ (a + 1) / 0 = a / 0 + if 0 ∣ a + 1 then 1 else 0
simp
no goals
a b m n k : ℕ
⊢ (0 + 1) / 1 = 0 / 1 + if 1 ∣ 0 + 1 then 1 else 0
simp
a b✝ m n k b : ℕ
hb2 : b + 2 > 1
⊢ (0 + 1) / (b + 2) = 0 / (b + 2) + if b + 2 ∣ 0 + 1 then 1 else 0
a b✝ m n k b : ℕ
⊢ (0 + 1) / (b + 2) = 0 / (b + 2) + if b + 2 ∣ 0 + 1 then 1 else 0
have hb2 : b + 2 > 1 := by simp
no goals
a b✝ m n k b : ℕ
hb2 : b + 2 > 1
⊢ (0 + 1) / (b + 2) = 0 / (b + 2) + if b + 2 ∣ 0 + 1 then 1 else 0
simp [ne_of_gt hb2, div_eq_of_lt hb2]
no goals
a b✝ m n k b : ℕ
⊢ b + 2 > 1
simp
a✝ b✝ m n k a b : ℕ
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (a + 1) / (b + 1) + if b + 1 ∣ a + 1 + 1 then 1 else 0
a✝ b✝ m n k a b : ℕ
⊢ (a + 1 + 1) / (b + 1) = (a + 1) / (b + 1) + if b + 1 ∣ a + 1 + 1 then 1 else 0
rw [Nat.div_eq]
a✝ b✝ m n k a b : ℕ
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
a✝ b✝ m n k a b : ℕ
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (a + 1) / (b + 1) + if b + 1 ∣ a + 1 + 1 then 1 else 0
conv_rhs => rw [Nat.div_eq]
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : b = a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0

case neg
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
a✝ b✝ m n k a b : ℕ
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
by_cases hb_eq_a : b = a + 1
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0

case neg
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : ¬b ≤ a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
case neg
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
by_cases hb_le_a1 : b ≤ a + 1
no goals
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : b = a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
simp [hb_eq_a, le_refl]
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
have hb_le_a : b ≤ a := le_of_lt_succ (lt_of_le_of_ne hb_le_a1 hb_eq_a)
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
have h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 := ⟨succ_pos _, (add_le_add_iff_right _).2 hb_le_a1⟩
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
have h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1 := ⟨succ_pos _, (add_le_add_iff_right _).2 hb_le_a⟩
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1
dvd_iff : b + 1 ∣ a - b + 1 ↔ b + 1 ∣ a + 1 + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
have dvd_iff : b + 1 ∣ a - b + 1 ↔ b + 1 ∣ a + 1 + 1 := by
  rw [Nat.dvd_add_iff_left (dvd_refl (b + 1)), ← add_tsub_add_eq_tsub_right a 1 b,
    add_comm (_ - _), add_assoc, tsub_add_cancel_of_le (succ_le_succ hb_le_a), add_comm 1]
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1
dvd_iff : b + 1 ∣ a - b + 1 ↔ b + 1 ∣ a + 1 + 1
wf : a - b < a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1
dvd_iff : b + 1 ∣ a - b + 1 ↔ b + 1 ∣ a + 1 + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
have wf : a - b < a + 1 := lt_succ_of_le tsub_le_self
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1
dvd_iff : b + 1 ∣ a - b + 1 ↔ b + 1 ∣ a + 1 + 1
wf : a - b < a + 1
⊢ ((a - b) / (b + 1) + if b + 1 ∣ a - b + 1 then 1 else 0) + 1 =
    (a - b) / (b + 1) + 1 + if b + 1 ∣ a + 1 + 1 then 1 else 0
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1
dvd_iff : b + 1 ∣ a - b + 1 ↔ b + 1 ∣ a + 1 + 1
wf : a - b < a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
rw [if_pos h₁, if_pos h₂, @add_tsub_add_eq_tsub_right, ← tsub_add_eq_add_tsub hb_le_a,
  have := wf
  succ_div (a - b),
  @add_tsub_add_eq_tsub_right]
no goals
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1
dvd_iff : b + 1 ∣ a - b + 1 ↔ b + 1 ∣ a + 1 + 1
wf : a - b < a + 1
⊢ ((a - b) / (b + 1) + if b + 1 ∣ a - b + 1 then 1 else 0) + 1 =
    (a - b) / (b + 1) + 1 + if b + 1 ∣ a + 1 + 1 then 1 else 0
simp [dvd_iff, succ_eq_add_one, add_comm 1, add_assoc]
no goals
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1
⊢ b + 1 ∣ a - b + 1 ↔ b + 1 ∣ a + 1 + 1
rw [Nat.dvd_add_iff_left (dvd_refl (b + 1)), ← add_tsub_add_eq_tsub_right a 1 b,
  add_comm (_ - _), add_assoc, tsub_add_cancel_of_le (succ_le_succ hb_le_a), add_comm 1]
case neg
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : ¬b ≤ a + 1
hba : ¬b ≤ a
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
case neg
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : ¬b ≤ a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
have hba : ¬b ≤ a := not_le_of_gt (lt_trans (lt_succ_self a) (lt_of_not_ge hb_le_a1))
case neg
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : ¬b ≤ a + 1
hba : ¬b ≤ a
hb_dvd_a : ¬b + 1 ∣ a + 2
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
case neg
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : ¬b ≤ a + 1
hba : ¬b ≤ a
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
have hb_dvd_a : ¬b + 1 ∣ a + 2 := fun h =>
  hb_le_a1 (le_of_succ_le_succ (le_of_dvd (succ_pos _) h))
no goals
case neg
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : ¬b ≤ a + 1
hba : ¬b ≤ a
hb_dvd_a : ¬b + 1 ∣ a + 2
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
simp [hba, hb_le_a1, hb_dvd_a]