English
Let R be a ring with a compatible order, and let x, y, z be points in an affine space over R. If both y and z lie on the segment from x toward the other (i.e., Wbtw R x y z and Wbtw R x z y), then y and z must be equal.
Русский
Пусть R — кольцо с совместимым порядком, возьмём точки x, y, z в аффинном пространстве над R. Если y и z оба лежат на отрезке от x к другому ( Wbtw R x y z и Wbtw R x z y ), то y = z.
LaTeX
$$$$ (Wbtw R x y z) \land (Wbtw R x z y) \leftrightarrow y = z $$$$
Lean4
theorem wbtw_swap_right_iff [NoZeroSMulDivisors R V] (x : P) {y z : P} : Wbtw R x y z ∧ Wbtw R x z y ↔ y = z :=
by
rw [wbtw_comm, wbtw_comm (z := y), eq_comm]
exact wbtw_swap_left_iff R x
