∀ {α : Type u_1} {l r : Ordnode α},
  ((∃ l', Ordnode.Raised l.size l' ∧ Ordnode.BalancedSz l' r.size) ∨
      ∃ r', Ordnode.Raised r' r.size ∧ Ordnode.BalancedSz l.size r') →
    (∃ l', Ordnode.Raised l' r.dual.size ∧ Ordnode.BalancedSz l' l.dual.size) ∨
      ∃ r', Ordnode.Raised l.dual.size r' ∧ Ordnode.BalancedSz r.dual.size r'