proposition: Lemma order_preserving_flip_nonneg (op : R -> R -> R) `{!Zero R} {E:forall z, PropHolds (0 ≤ z) -> OrderPreserving (fun y => op y z)} z : 0 ≤ z -> forall x y, x ≤ y -> op x z ≤ op y z.
proof: Proof. apply E. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.orders.orders HoTT.Classes.theory.apartness