proposition: Lemma strictly_order_preserving_pos (op : R → R → R) `{!Zero R} `{∀ z, PropHolds (0 < z) → StrictlyOrderPreserving (op z)} z : 0 < z → ∀ x y, x < y → op z x < op z y.
proof: Proof. firstorder. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.orders MathClasses.theory.setoids MathClasses.theory.strong_setoids