proposition: Lemma Rabs_Ropp : forall x:R, Rabs (- x) = Rabs x.
proof: Proof. intro; replace (-x) with (-1 * x) by ring. rewrite Rabs_mult. replace (Rabs (-1)) with 1. - apply Rmult_1_l. - unfold Rabs; case (Rcase_abs (-1)). + intro; ring. + rewrite <- Ropp_0. intro H0; apply Ropp_ge_cancel in H0. elim (Rge_not_lt _ _ H0). apply Rlt_0_1. Qed.
imports: Rdefinitions Raxioms RIneq R_Ifp