no goals
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ dual (node4L l x m y r) = node4R (dual r) y (dual m) x (dual l)
cases m <;> simp [node4L, node4R, node3R, dual_node3L, dual_node', add_comm]