{op} `{!Commutative op} `{!StrictlyOrderReflecting (op z) } : StrictlyOrderReflecting (fun y => op y z). Proof. intros x y E. apply (strictly_order_reflecting (op z)). rewrite 2!(commutativity (f:=op) z). trivial. Qed.
Require Import