mathlib3

e53aa870 - feat(order/basic): lemmas about `strict_mono_incr_on` (#4313)

feat(order/basic): lemmas about `strict_mono_incr_on` (#4313) Also move the section about `order_dual` up to use it in the proofs. Non-BC API changes: * Now `strict_mono_incr_on` and `strict_mono_decr_on` take `x` and `y` as `⦃⦄` args.