proposition: Lemma Rabs_minus_sym : forall x y:R, Rabs (x - y) = Rabs (y - x).
proof: Proof. intros; unfold Rabs; case (Rcase_abs (x - y)) as [Hlt|Hge]; case (Rcase_abs (y - x)) as [Hlt'|Hge']. - apply Rminus_lt, Rlt_asym in Hlt; apply Rminus_lt in Hlt'; contradiction. - rewrite (Ropp_minus_distr x y); trivial. - rewrite (Ropp_minus_distr y x); trivial. - destruct Hge; destruct Hge'. + apply Ropp_lt_gt_0_contravar in H; rewrite (Ropp_minus_distr x y) in H; apply Rlt_asym in H0; contradiction. + apply Rminus_diag_uniq in H0 as ->; trivial. + apply Rminus_diag_uniq in H as ->; trivial. + apply Rminus_diag_uniq in H0 as ->; trivial. Qed.
imports: Rdefinitions Raxioms RIneq R_Ifp