∀ {α : Type u_1} {β : α → Type u_2} (ls : ℕ) (lk : α) (lv : β lk) (ll lr : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).Balanced →
    ∀ (rs : ℕ) (rk : α) (rv : β rk),
      Std.DTreeMap.Internal.delta * ls < rs →
        ∀ (x : Std.DTreeMap.Internal.Impl α β),
          (Std.DTreeMap.Internal.Impl.inner rs rk rv Std.DTreeMap.Internal.Impl.leaf x).Balanced → False