proposition: Lemma Rabs_inv r : Rabs (/ r) = / Rabs r.
proof: Proof. unfold Rabs; case (Rcase_abs r) as [Hlt|Hge]; case (Rcase_abs (/ r)) as [Hlt'|Hge']; auto; intros. - apply eq_sym, Rinv_opp. - rewrite Rinv_opp. destruct Hge' as [| ->]. + apply Rinv_lt_0_compat, Rlt_asym in Hlt; contradiction. + rewrite Ropp_0; trivial. - destruct Hge as [H0| ->]. + apply Rinv_0_lt_compat, Rlt_asym in H0; contradiction. + rewrite Rinv_0. apply Ropp_0. Qed.
imports: Rdefinitions Raxioms RIneq R_Ifp