proposition: Lemma Rle_abs : forall x:R, x <= Rabs x.
proof: Proof. intro; unfold Rabs; case (Rcase_abs x); intros;auto with real. apply Rminus_le; rewrite <- Rplus_0_r; unfold Rminus; rewrite Ropp_involutive; auto with real. Qed.
imports: Rdefinitions Raxioms RIneq R_Ifp