proposition: Lemma RabsLUB : forall x y : R, (y < x -> False) /\ (y < - x -> False) <-> (y < Rabst (CReal_abs (Rrepr x)) -> False).
proof: Proof. split. - intros. rewrite Rlt_def in H0. apply CRealLtEpsilon in H0. rewrite Rquot2 in H0. destruct H. apply (CReal_abs_le (Rrepr x) (Rrepr y)). 2: exact H0. split. + apply (CReal_plus_le_reg_l (Rrepr y - Rrepr x)). ring_simplify. intro abs2. apply H1. rewrite Rlt_def. apply CRealLtForget. rewrite Rrepr_opp. exact abs2. + intro abs2. apply H. rewrite Rlt_def. apply CRealLtForget. exact abs2. - intros. split. + intro abs. apply H. rewrite Rlt_def. apply CRealLtForget. rewrite Rquot2. rewrite Rlt_def in abs. apply CRealLtEpsilon in abs. apply (CReal_lt_le_trans _ _ _ abs). apply CReal_le_abs. + intro abs. apply H. rewrite Rlt_def. apply CRealLtForget. rewrite Rquot2. rewrite Rlt_def in abs. apply CRealLtEpsilon in abs. apply (CReal_lt_le_trans _ _ _ abs). rewrite <- CReal_abs_opp, Rrepr_opp. apply CReal_le_abs. Qed.
imports: QArith_base Rdefinitions Raxioms ConstructiveReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveCauchyAbs ConstructiveRealsMorphisms