rw [← h1.left, div_add_mod (n + 1) 10]
case h.succ.left
n : ℕ
h1 :
  (match n.succ % 10 :: digits 10 (n.succ / 10) with
      | [] => default
      | a :: tail => a) =
      6 ∧
    ofDigits 10 (digits 10 (n.succ / 10) ++ [6]) = 4 * (n + 1)
⊢ n + 1 = 10 * ((n + 1) / 10) + 6
no goals