Circular order within one real turn

Increasing real representatives whose span is less than a full turn retain their strict circular order as angles. This graph-free fact supports horizontal ports and moving fans without requiring the same argument cut.

theorem Cslib.Polygonal.sbtw_angle_of_lt_of_span_lt {a b c : ℝ} (hab : a < b) (hbc : b < c) (hspan : c - a < 2 * Real.pi) : sbtw ↑a ↑b ↑c

Increasing real representatives with span less than a full turn give the literal counterclockwise strict angle order, without a principal-argument cut restriction.