∀ {α : Type u_1} [inst : Preorder α] {o₁ : WithBot α} {o₂ : WithTop α} {ls : ℕ} {ll lr : Ordnode α} {rs : ℕ}
  {rl : Ordnode α} {rx : α} {rr t : Ordnode α},
  3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1 →
    rl.size + rr.size ≤ 1 → Ordnode.Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs