proposition: Lemma strictly_order_preserving_flip {op} `{!Commutative op} `{!StrictlyOrderPreserving (op z)} : StrictlyOrderPreserving (fun y => op y z).
proof: Proof. intros x y E. rewrite 2!(commutativity _ z). apply strictly_order_preserving;trivial. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.orders.orders HoTT.Classes.theory.apartness