mathlib

f0c8a15d - chore(algebra/ordered_ring): golf some proofs using `strict_mono_incr_on` (#5323)