apply Nat.mod_eq_of_lt
case h₂.h₂.h₂
a b✝ c✝ b c : ℕ
⊢ ((b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)) % ((b + 1) * (c + 1)) =
    (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1)
case h₂.h₂.h₂.h
a b✝ c✝ b c : ℕ
⊢ (b + 1) * (a / (b + 1) % (c + 1)) + a % (b + 1) < (b + 1) * (c + 1)