proposition: Lemma preserving_preserves_nonneg : (∀ x, 0 ≤ x → 0 ≤ f x) → OrderPreserving f.
proof: Proof. intros E. repeat (split; try apply _). intros x y F. destruct (decompose_le F) as [z [Ez1 Ez2]]. apply compose_le with (f z). now apply E. now rewrite Ez2, preserves_plus. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings MathClasses.orders.orders MathClasses.orders.maps