English
If a configuration is valid with bounds o1,t,o2 and x sits above the nil bound, and all elements of t are strictly less than x, then the configuration with bound x is valid.
Русский
Если конфигурация допустима с границами o1,t,o2 и x выше нуля, причём все элементы t меньше 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 o_1 x) \\wedge (All(\\cdot < x) t)) \\Rightarrow Valid'(o_1,t,x).$$$
Lean4
theorem of_lt {t : Ordnode α} {x : α} {o₁ o₂} (H : Valid' o₁ t o₂) (h₁ : Bounded nil o₁ x) (h₂ : All (· < x) t) :
Valid' o₁ t x :=
⟨H.1.of_lt h₁ h₂, H.2, H.3⟩
