proposition: Lemma order_preserving_nonneg (op : R → R → R) `{!Zero R} `{∀ z, PropHolds (0 ≤ z) → OrderPreserving (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