proposition: Lemma order_reflecting_flip `{!Commutative op} `{!Proper ((=) ==> (=) ==> (=)) op} `{!OrderReflecting (op z) } : OrderReflecting (λ y, op y z).
proof: Proof. pose proof (order_morphism_mor (op z)). pose proof (setoidmor_a (op z)). repeat (split; try apply _). solve_proper. intros x y E. apply (order_reflecting (op z)). now rewrite 2!(commutativity z). Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.orders MathClasses.theory.setoids MathClasses.theory.strong_setoids