apply add_le_add
case h₂.h₂.h₂.h.h.a.a
a b✝ c✝ b c : ℕ
⊢ (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1) ≤ ?h₂.h₂.h₂.h.h.a.m

case h₂.h₂.h₂.h.h.a.m
a b✝ c✝ b c : ℕ
⊢ ℕ

case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ succ ?h₂.h₂.h₂.h.h.a.m ≤ (b + 1) * (c + 1)
case h₂.h₂.h₂.h.h.a.a.h₁
a b✝ c✝ b c : ℕ
⊢ (b + 1) * (a / (b + 1) % (c + 1)) ≤ ?h₂.h₂.h₂.h.h.a.a.b

case h₂.h₂.h₂.h.h.a.a.h₂
a b✝ c✝ b c : ℕ
⊢ a % (b + 1) ≤ ?h₂.h₂.h₂.h.h.a.a.d

case h₂.h₂.h₂.h.h.a.a.b
a b✝ c✝ b c : ℕ
⊢ ℕ

case h₂.h₂.h₂.h.h.a.a.d
a b✝ c✝ b c : ℕ
⊢ ℕ

case h₂.h₂.h₂.h.h.a
a b✝ c✝ b c : ℕ
⊢ succ (?h₂.h₂.h₂.h.h.a.a.b + ?h₂.h₂.h₂.h.h.a.a.d) ≤ (b + 1) * (c + 1)