case node
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ All P (if size l✝ < ratio * size r✝ then node3L l x l✝ x✝ r✝ else node4L l x l✝ x✝ r✝) ↔
    All P l ∧ P x ∧ All P (node size✝ l✝ x✝ r✝)
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
⊢ All P (rotateL l x r) ↔ All P l ∧ P x ∧ All P r
cases r <;> simp [rotateL, all_node']
no goals
case node
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ All P (if size l✝ < ratio * size r✝ then node3L l x l✝ x✝ r✝ else node4L l x l✝ x✝ r✝) ↔
    All P l ∧ P x ∧ All P (node size✝ l✝ x✝ r✝)
split_ifs <;>
simp [all_node3L, all_node4L, All, and_assoc]