English
In a totally ordered type, inserting x into t and then taking the dual is the same as inserting x into the dual of t, i.e., dual(insert x t) = insert x (dual t).
Русский
В полностью упорядоченном типе вставка x в t и затем двойственное преобразование даёт то же самое, что вставка x в двойственное дерево t: dual(insert x t) = insert x (dual t).
LaTeX
$$dual(Ordnode.insert x t) = Ordnode.insert x (dual t)$$
Lean4
theorem dual_insert [LE α] [IsTotal α (· ≤ ·)] [DecidableLE α] (x : α) :
∀ t : Ordnode α, dual (Ordnode.insert x t) = @Ordnode.insert αᵒᵈ _ _ x (dual t)
| nil => rfl
| node _ l y r => by
have : @cmpLE αᵒᵈ _ _ x y = cmpLE y x := rfl
rw [Ordnode.insert, dual, Ordnode.insert, this, ← cmpLE_swap x y]
cases cmpLE x y <;> simp [Ordering.swap, dual_balanceL, dual_balanceR, dual_insert]
