∀ {s : String} {q : s.Pos} {r : ℕ} (p : s.Pos) (acc : ℕ) (h : ¬p = s.endPos) (d : ℕ)
  (motive :
    (k : ℕ) →
      (0 < k → Lean.parseLowerHex?✝ k s (p.next h) (acc <<< 4 ||| d) = some (q, r) → p.next h < q) → 0 < k.succ → Prop)
  (k : ℕ) (ih : 0 < k → Lean.parseLowerHex?✝¹ k s (p.next h) (acc <<< 4 ||| d) = some (q, r) → p.next h < q)
  (hk : 0 < k.succ),
  (∀ (ih : 0 < 0 → Lean.parseLowerHex?✝² 0 s (p.next h) (acc <<< 4 ||| d) = some (q, r) → p.next h < q)
      (hk : 0 < Nat.succ 0), motive 0 ih hk) →
    (∀ (k : ℕ)
        (ih : 0 < k + 1 → Lean.parseLowerHex?✝³ (k + 1) s (p.next h) (acc <<< 4 ||| d) = some (q, r) → p.next h < q)
        (hk : 0 < (k + 1).succ), motive k.succ ih hk) →
      motive k ih hk