English
Strict between is cyclic: sbtw a b c iff sbtw c a b.
Русский
Строгое между циклично: sbtw a b c эквивално sbtw c a b.
LaTeX
$$$\\forall a,b,c:\\alpha,\\ sbtw(a,b,c) \\iff sbtw(c,a,b)$$$
Lean4
/-- The order of the `↔` has been chosen so that `rw [sbtw_cyclic]` cycles to the right while
`rw [← sbtw_cyclic]` cycles to the left (thus following the prepended arrow). -/
theorem sbtw_cyclic {a b c : α} : sbtw a b c ↔ sbtw c a b :=
⟨sbtw_cyclic_right, sbtw_cyclic_left⟩
-- TODO: `alias` creates a def instead of a lemma (because `sbtw_trans_left` is a def).
-- alias btw_trans_left ← SBtw.sbtw.trans_left
