(forall x, 0 ≤ x -> 0 ≤ f x) -> OrderPreserving f. 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). - apply E;trivial. - rewrite Ez2, (preserves_plus (f:=f)). trivial. Qed.
Require Import