proposition: Lemma continuous_imp_continuous' : forall (A B : CPsMetricSpace) (f : CSetoid_fun A B), continuous f -> continuous' f.
proof: Proof. intros A B f. unfold continuous in |- *. intro H. unfold continuous' in |- *. intros x n. set (H1 := two_ap_zero IR) in *. elim H with x (S n) H1. intros p H2. exists (power p 2). intro y. intro H3. apply leEq_transitive with ((OneR[/] Two:IR[//]H1)[^]S n). apply less_leEq. apply H2. apply leEq_less_trans with (one_div_succ (R:=IR) (power p 2)). exact H3. unfold one_div_succ in |- *. astepr (OneR[^]p[/] (Two:IR)[^]p[//]nexp_resp_ap_zero p H1). astepr (OneR[/] (Two:IR)[^]p[//]nexp_resp_ap_zero p H1). apply recip_resp_less. apply nexp_resp_pos. apply pos_two. unfold Snring in |- *. apply less_wdr with (nexp IR p Two[+][1]). apply shift_less_plus. apply minusOne_less. astepl (OneR[+]nexp IR p Two). stepr (OneR[+]nring (power p 2)). apply plus_resp_eq. apply nexp_power. simpl in |- *. algebra. apply less_leEq. astepl (OneR[^]S n[/] (Two:IR)[^]S n[//]nexp_resp_ap_zero (S n) H1). astepl (OneR[/] (Two:IR)[^]S n[//]nexp_resp_ap_zero (S n) H1). unfold one_div_succ in |- *. unfold Snring in |- *. apply bin_less_un. Qed.
imports: CoRN.metrics.CPseudoMSpaces