Documentation

Mathlib.Data.Real.StarOrdered