mathlib3

f118c146 - feat(order): if `f x ≤ f y → x ≤ y`, then `f` is injective (#8373)

feat(order): if `f x ≤ f y → x ≤ y`, then `f` is injective (#8373) I couldn't find this specific result, not assuming linear orders, anywhere and [the Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/If.20.60f.20x.20.E2.89.A4.20f.20y.20.E2.86.92.20x.20.E2.89.A4.20y.60.2C.20then.20.60f.60.20is.20injective) didn't get any responses, so I decided to PR the result. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>