α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ dual
      (if size l + size r ≤ 1 then node' l x r
      else
        if delta * size l < size r then rotateL l x r
        else if delta * size r < size l then rotateR l x r else node' l x r) =
    if size l + size r ≤ 1 then node' (dual r) x (dual l)
    else
      if delta * size r < size l then rotateL (dual r) x (dual l)
      else if delta * size l < size r then rotateR (dual r) x (dual l) else node' (dual r) x (dual l)
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ dual (balance' l x r) = balance' (dual r) x (dual l)
simp [balance', add_comm]
case inr.inl.inl
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
h : ¬size l + size r ≤ 1
h_1 : delta * size l < size r
h_2 : delta * size r < size l
⊢ rotateR (dual r) x (dual l) = rotateL (dual r) x (dual l)
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ dual
      (if size l + size r ≤ 1 then node' l x r
      else
        if delta * size l < size r then rotateL l x r
        else if delta * size r < size l then rotateR l x r else node' l x r) =
    if size l + size r ≤ 1 then node' (dual r) x (dual l)
    else
      if delta * size r < size l then rotateL (dual r) x (dual l)
      else if delta * size l < size r then rotateR (dual r) x (dual l) else node' (dual r) x (dual l)
split_ifs with h h_1 h_2 <;>
simp [dual_node', dual_rotateL, dual_rotateR, add_comm]
no goals
case inr.inl.inl
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
h : ¬size l + size r ≤ 1
h_1 : delta * size l < size r
h_2 : delta * size r < size l
⊢ rotateR (dual r) x (dual l) = rotateL (dual r) x (dual l)
cases delta_lt_false h_1 h_2