proposition: Lemma uni_continuous_imp_uni_continuous' : forall (A B : CPsMetricSpace) (f : CSetoid_fun A B), uni_continuous f -> uni_continuous' f.
proof: Proof. intros A B f. unfold uni_continuous in |- *. intro H. unfold uni_continuous' in |- *. intro n. set (H0 := two_ap_zero IR) in *. elim H with (S n) H0. intros p H1. exists (power p 2). intros x y H2. apply less_leEq. apply less_transitive_unfolded with ((OneR[/] Two:IR[//]H0)[^]S n). apply H1. apply leEq_less_trans with (one_div_succ (R:=IR) (power p 2)). exact H2. unfold one_div_succ in |- *. unfold Snring in |- *. astepr (OneR[^]p[/] (Two:IR)[^]p[//]nexp_resp_ap_zero p H0). astepr (OneR[/] (Two:IR)[^]p[//]nexp_resp_ap_zero p H0). apply recip_resp_less. apply nexp_resp_pos. apply pos_two. astepr (nring (R:=IR) (power p 2)[+][1]). astepl (nexp IR p Two[+][0]). apply plus_resp_leEq_less. apply eq_imp_leEq. apply nexp_power. apply pos_one. unfold one_div_succ in |- *. unfold Snring in |- *. astepl (OneR[^]S n[/] (Two:IR)[^]S n[//]nexp_resp_ap_zero (S n) H0). astepl (OneR[/] (Two:IR)[^]S n[//]nexp_resp_ap_zero (S n) H0). apply bin_less_un. Qed.
imports: CoRN.metrics.CPseudoMSpaces