proposition: Lemma Rabs_def2 : forall x a:R, Rabs x < a -> x < a /\ - a < x.
proof: Proof. unfold Rabs; intro x; case (Rcase_abs x) as [Hlt|Hge]; intros. - generalize (Ropp_gt_lt_0_contravar x Hlt); unfold Rgt; intro; generalize (Rlt_trans 0 (- x) a H0 H); intro; split. + apply (Rlt_trans x 0 a Hlt H1). + generalize (Ropp_lt_gt_contravar (- x) a H); rewrite (Ropp_involutive x); unfold Rgt; trivial. - fold (a > x) in H; generalize (Rgt_ge_trans a x 0 H Hge); intro; generalize (Ropp_lt_gt_0_contravar a H0); intro; fold (0 > - a); generalize (Rge_gt_trans x 0 (- a) Hge H1); unfold Rgt; intro; split; assumption. Qed.
imports: Rdefinitions Raxioms RIneq R_Ifp