∀ {α : Type u_1} [inst : Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
  Ordnode.Valid' o₁ l ↑x →
    Ordnode.Valid' (↑x) r o₂ →
      ¬l.size + r.size ≤ 1 →
        Ordnode.delta * r.size < l.size →
          2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3 → Ordnode.Valid' o₁ (l.rotateR x r) o₂