Lean4
/-- The circular order obtained from "looping around" a linear order.
See note [reducible non-instances]. -/
abbrev toCircularOrder (α : Type*) [LinearOrder α] : CircularOrder α :=
{ PartialOrder.toCircularPartialOrder α with
btw_total := fun a b c =>
by
rcases le_total a b with hab | hba <;> rcases le_total b c with hbc | hcb <;> rcases le_total c a with hca | hac
· exact Or.inl (Or.inl ⟨hab, hbc⟩)
· exact Or.inl (Or.inl ⟨hab, hbc⟩)
· exact Or.inl (Or.inr <| Or.inr ⟨hca, hab⟩)
· exact Or.inr (Or.inr <| Or.inr ⟨hac, hcb⟩)
· exact Or.inl (Or.inr <| Or.inl ⟨hbc, hca⟩)
· exact Or.inr (Or.inr <| Or.inl ⟨hba, hac⟩)
· exact Or.inr (Or.inl ⟨hcb, hba⟩)
· exact Or.inr (Or.inr <| Or.inl ⟨hba, hac⟩) }
