pub open spec fn total_ordering<T>(r: FnSpec<(T, T), bool>) -> bool
{ &&& reflexive(r) &&& antisymmetric(r) &&& transitive(r) &&& strongly_connected(r) }