∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α) (size : ℕ) (ky : α) (y : β)
  (l r : Std.DTreeMap.Internal.Impl α fun x => β) (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, (compare a k).isGE = true),
  Std.DTreeMap.Internal.Impl.Const.getEntryGE k (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he =
    match h : compare k ky with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.Const.getEntryGED k l (ky, y)
    | Ordering.eq => (ky, y)
    | Ordering.gt => Std.DTreeMap.Internal.Impl.Const.getEntryGE k r ⋯ ⋯