proposition: Lemma Cexis_AFS_CC : forall x y eps, [0] [<] eps -> {y' : CC | AbsSmallCC eps (y'[-]y) | y' [#] x}.
proof: Proof. unfold AbsSmallCC in |- *. intros. set (e := cc_IR eps) in *. elim (ap_cotransitive_unfolded _ (y[-]e) (y[+]e)) with x; try intro H0. exists (y[-]e). apply leEq_wdl with (AbsCC [--]e). unfold e in |- *. astepl (AbsCC (cc_IR eps)). apply eq_imp_leEq. apply AbsCC_IR. apply less_leEq; auto. apply AbsCC_wd. rational. auto. exists (y[+]e). apply leEq_wdl with (AbsCC e). apply eq_imp_leEq. unfold e in |- *; apply AbsCC_IR. apply less_leEq; auto. apply AbsCC_wd. rational. apply ap_symmetric_unfolded. auto. apply zero_minus_apart. apply ap_wdl_unfolded with (cc_IR ( [--]Two[*]eps)). astepr (cc_IR [0]). apply cc_IR_resp_ap. apply mult_resp_ap_zero. apply inv_resp_ap_zero. apply two_ap_zero. apply pos_ap_zero; auto. unfold e in |- *. astepl (cc_IR [--]Two[*]cc_IR eps). rstepr ( [--]Two[*]cc_IR eps). apply mult_wdl. simpl in |- *. unfold cc_eq in |- *. simpl in |- *. split; [ algebra | rational ]. Qed.
imports: CoRN.complex.CComplex