∀ {α : Type u} {β : α → Type v} [o : Ord α] [Std.TransOrd α] {t : Std.DTreeMap.Internal.Impl α β} {k : α},
  Std.DTreeMap.Internal.Impl.getEntryLT? k t = Std.DTreeMap.Internal.Impl.getEntryGT? k t.reverse