mathlib3

506ad313 - feat(order/monotone): simp lemmas for monotonicity in dual orders (#13207)

feat(order/monotone): simp lemmas for monotonicity in dual orders (#13207) Add 4 lemmas of the kind `antitone_to_dual_comp_iff` Add their variants for `antitone_on` Add their strict variants Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr> Co-authored-by: YaelDillies <yael.dillies@gmail.com>