proposition: Lemma reflecting_preserves_nonneg : (∀ x, 0 ≤ f x → 0 ≤ x) → OrderReflecting f.
proof: Proof. intros E. repeat (split; try apply _). intros x y F. apply flip_nonneg_minus, E. rewrite preserves_plus, preserves_negate. now apply flip_nonneg_minus, F. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings MathClasses.orders.semirings