(forall x, 0 ≤ f x -> 0 ≤ x) -> OrderReflecting f. Proof. intros E. repeat (split; try apply _). intros x y F. apply flip_nonneg_minus, E. rewrite preserves_plus, preserves_negate. apply (flip_nonneg_minus (f x)), F. Qed.
Require Import