proposition: Lemma Rabs_pos : forall x:R, 0 <= Rabs x.
proof: Proof. intros; unfold Rabs; case (Rcase_abs x) as [Hlt|Hge]. - generalize (Ropp_lt_gt_contravar x 0 Hlt); intro; unfold Rgt in H; rewrite Ropp_0 in H; left; assumption. - apply Rge_le; assumption. Qed.
imports: Rdefinitions Raxioms RIneq R_Ifp