English
If a configuration is valid with bounds o1,t, and t is all elements strictly greater than x, and x is bounded nil to o2, then the configuration with bound x is valid.
Русский
Если конфигурация допустима с границами o1,t, и все элементы t строго больше x, а nil ограничено x слева, то конфигурация с нижней границей x допустима.
LaTeX
$$$\\forall t:\\ Ordnode(\\alpha), \\forall x:\\alpha, \\forall o_1,o_2,\\; (H : Valid'(o_1,t,o_2)) \\Rightarrow ((Bounded nil x o_2) \\wedge (All(\\cdot > x) t)) \\Rightarrow Valid'(x,t,o_2).$$$
Lean4
theorem of_gt {t : Ordnode α} {x : α} {o₁ o₂} (H : Valid' o₁ t o₂) (h₁ : Bounded nil x o₂) (h₂ : All (· > x) t) :
Valid' x t o₂ :=
⟨H.1.of_gt h₁ h₂, H.2, H.3⟩
