proposition: Lemma C_complete_ax1 : forall F : (C -> Prop) -> Prop, ProperFilter F -> (forall eps : posreal, exists x : C, F (ball x eps)) -> forall eps : posreal, F (ball (C_complete_lim F) eps).
proof: Proof. intros. apply filter_and ; simpl ; revert eps. apply (R_complete (fun P => F (fun z => P (Re z)))). split ; intros. destruct (filter_ex _ H1). by exists (Re x). split. by apply filter_true. intros ; by apply filter_and. intros ; eapply filter_imp, H2. intros ; by apply H1. intros ; destruct (H0 eps). exists (Re x). move: H1 ; apply filter_imp. intros ; by apply H1. apply (R_complete (fun P => F (fun z => P (Im z)))). split ; intros. destruct (filter_ex _ H1). by exists (Im x). split. by apply filter_true. intros ; by apply filter_and. intros ; eapply filter_imp, H2. intros ; by apply H1. intros ; destruct (H0 eps). exists (Im x). move: H1 ; apply filter_imp. intros ; by apply H1. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy