Real representatives of a finite directed circular order

A finite clockwise enumeration admits real angle representatives in one open turn, in reverse linear order. The argument cut is chosen in the prescribed gap before the last clockwise entry. Singleton enumerations are included.

theorem Cslib.Polygonal.exists_reverse_ordered_angle_lift (n : ℕ) (dir : Fin (n + 1) → Real.Angle) (hinj : Function.Injective dir) (horder : ∀ (i j : Fin (n + 1)), i ≠ Fin.last n → j ≠ Fin.last n → i ≠ j → (sbtw (dir (Fin.last n)) (dir i) (dir j) ↔ ↑j < ↑i)) : ∃ (cut : ℝ) (L : Real.Angle → ℝ), (∀ (i : Fin (n + 1)), L (dir i) ∈ Set.Ioo cut (cut + 2 * Real.pi)) ∧ (∀ (φ : Real.Angle), ↑(L φ) = φ) ∧ ∀ (i j : Fin (n + 1)), L (dir i) < L (dir j) ↔ ↑j < ↑i

Choose one open turn of real representatives for a finite clockwise enumeration. Only the circular order at its specified last entry is needed.