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