proposition: Lemma abs_mult (x y : R) : abs (x * y) = abs x * abs y.
proof: Proof. Proof with try ring; auto. destruct (total (≤) 0 x) as [Ex|Ex]; destruct (total (≤) 0 y) as [Ey|Ey]. rewrite ?abs_nonneg... apply nonneg_mult_compat... rewrite (abs_nonneg x), (abs_nonpos y), (abs_nonpos (x * y))... apply nonneg_nonpos_mult... rewrite (abs_nonpos x), (abs_nonneg y), (abs_nonpos (x * y))... apply nonpos_nonneg_mult... rewrite (abs_nonpos x), (abs_nonpos y), (abs_nonneg (x * y))... apply nonpos_mult... Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.rings