proposition: Lemma Rabs_left : forall r, r < 0 -> Rabs r = - r.
proof: Proof. intros; unfold Rabs; case (Rcase_abs r); trivial; intro; absurd (r >= 0). - exact (Rlt_not_ge r 0 H). - assumption. Qed.
imports: Rdefinitions Raxioms RIneq R_Ifp