∀ {α : Type u} {β : Type v} (x : Std.DTreeMap.Internal.Impl α fun x => β) (x_1 : ℕ),
  Std.DTreeMap.Internal.Impl.Const.entryAtIdx? x x_1 =
    match x, x_1 with
    | Std.DTreeMap.Internal.Impl.leaf, x => none
    | Std.DTreeMap.Internal.Impl.inner size k v l r, n =>
      match compare n l.size with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.Const.entryAtIdx? l n
      | Ordering.eq => some (k, v)
      | Ordering.gt => Std.DTreeMap.Internal.Impl.Const.entryAtIdx? r (n - l.size - 1)