{op} `{!Commutative op} `{!StrictlyOrderPreserving (op z)} : StrictlyOrderPreserving (fun y => op y z). Proof. intros x y E. rewrite 2!(commutativity _ z). apply strictly_order_preserving;trivial. Qed.
Require Import