proposition: Lemma Rabs_right : forall r, r >= 0 -> Rabs r = r.
proof: Proof. intros; unfold Rabs; case (Rcase_abs r) as [Hlt|Hge]. - absurd (r >= 0). + exact (Rlt_not_ge r 0 Hlt). + assumption. - trivial. Qed.
imports: Rdefinitions Raxioms RIneq R_Ifp