English
The dual of a valid' structure is valid' in the dual order, and conversely via the dual operation.
Русский
Дуальность допустимой структуры в двойственном порядке сохраняется и обратно возвращается через операцию двойственности.
LaTeX
$$$\\forall t,o_1,o_2:\\; \\operatorname{Ordnode.Valid}'(o_1,t,o_2) \\Rightarrow @\\operatorname{Valid}'(\\alpha^{\\mathrm{op}}, o_2, (dual\ t)).$$$
Lean4
theorem dual : ∀ {t : Ordnode α} {o₁ o₂}, Valid' o₁ t o₂ → @Valid' αᵒᵈ _ o₂ (dual t) o₁
| .nil, _, _, h => valid'_nil h.1.dual
| .node _ l _ r, _, _, ⟨⟨ol, Or⟩, ⟨rfl, sl, sr⟩, ⟨b, bl, br⟩⟩ =>
let ⟨ol', sl', bl'⟩ := Valid'.dual ⟨ol, sl, bl⟩
let ⟨or', sr', br'⟩ := Valid'.dual ⟨Or, sr, br⟩
⟨⟨or', ol'⟩, ⟨by simp [size_dual, add_comm], sr', sl'⟩, ⟨by rw [size_dual, size_dual]; exact b.symm, br', bl'⟩⟩
