proposition: Lemma Rabs_mult : forall x y:R, Rabs (x * y) = Rabs x * Rabs y.
proof: Proof. intros; unfold Rabs; case (Rcase_abs (x * y)) as [Hlt|Hge]; case (Rcase_abs x) as [Hltx|Hgex]; case (Rcase_abs y) as [Hlty|Hgey]; auto. - apply Rmult_lt_gt_compat_neg_l with (r:=x), Rlt_asym in Hlty; trivial. rewrite Rmult_0_r in Hlty; contradiction. - rewrite (Ropp_mult_distr_l_reverse x y); trivial. - rewrite (Rmult_comm x (- y)); rewrite (Ropp_mult_distr_l_reverse y x); rewrite (Rmult_comm x y); trivial. - destruct Hgex as [| ->], Hgey as [| ->]. + apply Rmult_lt_compat_l with (r:=x), Rlt_asym in H0; trivial. rewrite Rmult_0_r in H0; contradiction. + rewrite Rmult_0_r in Hlt; contradiction (Rlt_irrefl 0). + rewrite Rmult_0_l in Hlt; contradiction (Rlt_irrefl 0). + rewrite Rmult_0_l in Hlt; contradiction (Rlt_irrefl 0). - rewrite (Rmult_opp_opp x y); trivial. - destruct Hge. + destruct Hgey. * apply Rmult_lt_compat_r with (r:=y), Rlt_asym in Hltx; trivial. rewrite Rmult_0_l in Hltx; contradiction. * rewrite H0, Rmult_0_r in H; contradiction (Rlt_irrefl 0). + rewrite <- Ropp_mult_distr_l, H, Ropp_0; trivial. - destruct Hge. + destruct Hgex. * apply Rmult_lt_compat_l with (r:=x), Rlt_asym in Hlty; trivial. rewrite Rmult_0_r in Hlty; contradiction. * rewrite H0, 2!Rmult_0_l; trivial. + rewrite <- Ropp_mult_distr_r, H, Ropp_0; trivial. Qed.
imports: Rdefinitions Raxioms RIneq R_Ifp