obtain ⟨_ | _ | c, rfl⟩ := hdvd
a b : ℕ
ha : a ≠ 0
hdvd : b ∣ a
hlt : a < 2 * b
⊢ a = b
case intro.zero
b : ℕ
ha : b * 0 ≠ 0
hlt : b * 0 < 2 * b
⊢ b * 0 = b

case intro.succ.zero
b : ℕ
ha : b * (0 + 1) ≠ 0
hlt : b * (0 + 1) < 2 * b
⊢ b * (0 + 1) = b

case intro.succ.succ
b c : ℕ
ha : b * (c + 1 + 1) ≠ 0
hlt : b * (c + 1 + 1) < 2 * b
⊢ b * (c + 1 + 1) = b