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