α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
⊢ All P (dual r) ∧ P x ∧ All P (dual l) ↔ All P l ∧ P x ∧ All P r
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
⊢ All P (rotateR l x r) ↔ All P l ∧ P x ∧ All P r
rw [← all_dual, dual_rotateR, all_rotateL]
no goals
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
⊢ All P (dual r) ∧ P x ∧ All P (dual l) ↔ All P l ∧ P x ∧ All P r
simp [all_dual, and_comm, and_left_comm, and_assoc]