α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
⊢ All P
      (if size l + size r ≤ 1 then node' l x r
      else
        if size r > delta * size l then rotateL l x r
        else if size l > delta * size r then rotateR l x r else node' l x r) ↔
    All P l ∧ P x ∧ All P r
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
⊢ All P (balance' l x r) ↔ All P l ∧ P x ∧ All P r
rw [balance']
no goals
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
⊢ All P
      (if size l + size r ≤ 1 then node' l x r
      else
        if size r > delta * size l then rotateL l x r
        else if size l > delta * size r then rotateR l x r else node' l x r) ↔
    All P l ∧ P x ∧ All P r
split_ifs <;> simp [all_node', all_rotateL, all_rotateR]