proposition: Lemma Rabs_def1 : forall x a:R, x < a -> - a < x -> Rabs x < a.
proof: Proof. unfold Rabs; intros; case (Rcase_abs x); intro. - generalize (Ropp_lt_gt_contravar (- a) x H0); unfold Rgt; rewrite Ropp_involutive; intro; assumption. - assumption. Qed.
imports: Rdefinitions Raxioms RIneq R_Ifp