le_implies_le_of_le_of_le

monotonicity of ≤ with respect to →

ordering.compares

compares o a b means that a and b have the ordering relation o between them, assuming that the relation a < b is defined