proposition: Lemma reflecting_preserves_nonneg : (forall 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. apply (flip_nonneg_minus (f x)), F. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.groups HoTT.Classes.theory.rings HoTT.Classes.orders.semirings