∀ {α : Type u_1} {β : α → Type u_2} (rs : ℕ) (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner rs k v l r).Balanced →
    ∀ (ls : ℕ) (lk : α) (lv : β lk),
      Std.DTreeMap.Internal.delta * rs < ls →
        ∀ (size : ℕ) (k_1 : α) (v_1 : β k_1) (l_1 r_1 : Std.DTreeMap.Internal.Impl α β),
          (Std.DTreeMap.Internal.Impl.inner ls lk lv (Std.DTreeMap.Internal.Impl.inner size k_1 v_1 l_1 r_1)
                Std.DTreeMap.Internal.Impl.leaf).Balanced →
            Std.DTreeMap.Internal.Impl.BalanceLErasePrecond
                (Std.DTreeMap.Internal.Impl.inner ls lk lv (Std.DTreeMap.Internal.Impl.inner size k_1 v_1 l_1 r_1)
                    Std.DTreeMap.Internal.Impl.leaf).size
                (Std.DTreeMap.Internal.Impl.inner rs k v l r).size →
              False