proposition: Lemma abs_negate (x : R) : abs (-x) = abs x.
proof: Proof. Proof with trivial. destruct (total (≤) 0 x). rewrite (abs_nonneg x), abs_nonpos... apply rings.negate_involutive. apply flip_nonneg_negate... rewrite (abs_nonneg (-x)), abs_nonpos... reflexivity. apply flip_nonpos_negate... Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.rings