case node
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ dual (if size l✝ < ratio * size r✝ then node3L l x l✝ x✝ r✝ else node4L l x l✝ x✝ r✝) =
    if size l✝ < ratio * size r✝ then node3R (dual r✝) x✝ (dual l✝) x (dual l)
    else node4R (dual r✝) x✝ (dual l✝) x (dual l)
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ dual (rotateL l x r) = rotateR (dual r) x (dual l)
cases r <;> simp [rotateL, rotateR, dual_node']
no goals
case node
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ dual (if size l✝ < ratio * size r✝ then node3L l x l✝ x✝ r✝ else node4L l x l✝ x✝ r✝) =
    if size l✝ < ratio * size r✝ then node3R (dual r✝) x✝ (dual l✝) x (dual l)
    else node4R (dual r✝) x✝ (dual l✝) x (dual l)
split_ifs <;>
simp [dual_node3L, dual_node4L, node3R, add_comm]