proposition: Lemma Rabs_pos_eq : forall x:R, 0 <= x -> Rabs x = x.
proof: Proof. intros; unfold Rabs; case (Rcase_abs x) as [Hlt|Hge]; [ generalize (Rgt_not_le 0 x Hlt); intro; exfalso; auto | trivial ]. Qed.
imports: Rdefinitions Raxioms RIneq R_Ifp