∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β) (lowerBound : α)
  (it : Std.DTreeMap.Internal.Zipper α β),
  Std.DTreeMap.Internal.Zipper.prependMapGE t lowerBound it =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf => it
    | Std.DTreeMap.Internal.Impl.inner size k v l r =>
      match compare lowerBound k with
      | Ordering.lt =>
        Std.DTreeMap.Internal.Zipper.prependMapGE l lowerBound (Std.DTreeMap.Internal.Zipper.cons k v r it)
      | Ordering.eq => Std.DTreeMap.Internal.Zipper.cons k v r it
      | Ordering.gt => Std.DTreeMap.Internal.Zipper.prependMapGE r lowerBound it