proposition: Lemma preserves_abs x : f (abs x) = abs (f x).
proof: Proof. destruct (total (≤) 0 x). rewrite ?abs_nonneg; try easy. now apply semirings.preserves_nonneg. rewrite ?abs_nonpos; try easy. apply rings.preserves_negate. now apply preserves_nonpos. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.rings