English
If h is a witness that x lies between y and z, then Wbtw R z x y holds exactly when x = y.
Русский
Если имеется свидетельство того, что x лежит между y и z, то Wbtw R z x y верно тогда и только тогда, когда x = y.
LaTeX
$$$$ \text{If } h: Wbtw R x y z, \quad Wbtw R z x y \leftrightarrow x = y $$$$
Lean4
theorem rotate_iff [NoZeroSMulDivisors R V] {x y z : P} (h : Wbtw R x y z) : Wbtw R z x y ↔ x = y := by
rw [← wbtw_rotate_iff R x, and_iff_right h]