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