proposition: Lemma plus_resp_continuous : forall (X : CPsMetricSpace) (f g : CSetoid_fun X IR_as_CPsMetricSpace) (H : continuous f) (H1 : continuous g), continuous (compose_CSetoid_bin_fun X IR_as_CPsMetricSpace IR_as_CPsMetricSpace f g (csg_op (c:=IR))).
proof: Proof. unfold continuous in |- *. simpl in |- *. unfold dIR in |- *. intros X f g H H0. intros x n H1. simpl in |- *. elim (H x (S n) H1). intros xn H2. elim (H0 x (S n) H1). intros x0 H3. exists (Nat.max xn x0). intros y H6. astepl (ABSIR (f x[-]f y[+](g x[-]g y))). apply leEq_less_trans with (ABSIR (f x[-]f y)[+]ABSIR (g x[-]g y)). apply IR_tri_ineq. apply less_leEq_trans with ((OneR[/] [0][+][1][+][1][//]H1)[^]S n[+]ABSIR (g x[-]g y)). apply plus_resp_less_rht. apply H2. apply less_leEq_trans with (nexp IR (Nat.max xn x0) ([1][/] [0][+][1][+][1][//]H1)). exact H6. astepl ((OneR[/] [0][+][1][+][1][//]H1)[^]Nat.max xn x0). astepr ((OneR[/] [0][+][1][+][1][//]H1)[^]xn). apply small_nexp_resp_le. apply shift_leEq_div. astepr (Two:IR). apply pos_two. astepl ZeroR. apply less_leEq. apply pos_one. apply shift_div_leEq. astepr (Two:IR). apply pos_two. astepr (OneR[+][1]). astepr (Two:IR). apply less_leEq. apply one_less_two. rational. intuition. apply leEq_transitive with ((OneR[/] [0][+][1][+][1][//]H1)[^]S n[+] ([1][/] [0][+][1][+][1][//]H1)[^]S n). apply plus_resp_leEq_lft. apply less_leEq. apply H3. apply less_leEq_trans with (nexp IR (Nat.max xn x0) ([1][/] [0][+][1][+][1][//]H1)). exact H6. astepl ((OneR[/] [0][+][1][+][1][//]H1)[^]Nat.max xn x0). astepr ((OneR[/] [0][+][1][+][1][//]H1)[^]x0). apply small_nexp_resp_le. apply shift_leEq_div. astepr (Two:IR). apply pos_two. astepl ZeroR. apply less_leEq. apply pos_one. apply shift_div_leEq. astepr (Two:IR). apply pos_two. astepr (OneR[+][1]). astepr (Two:IR). apply less_leEq. apply one_less_two. rational. intuition. apply eq_imp_leEq. astepl ((Two:IR)[*]([1][/] [0][+][1][+][1][//]H1)[^]S n). astepr ((OneR[/] [0][+][1][+][1][//]H1)[^]n). astepl ((Two:IR)[*] ([1][^]S n[/] ([0][+][1][+][1])[^]S n[//]nexp_resp_ap_zero (S n) H1)). astepl ((Two:IR)[*]([1][/] ([0][+][1][+][1])[^]S n[//]nexp_resp_ap_zero (S n) H1)). astepl ((Two:IR)[*] (([1][/] ([0][+][1][+][1])[^]n[//]nexp_resp_ap_zero n H1)[*] ([1][/] [0][+][1][+][1][//]H1))). 2: apply mult_wdr. 2: astepl (([1][/] [0][+][1][+][1][//]H1)[^]S n). 3: astepl (([1][/] [0][+][1][+][1][//]H1)[^]n[*]([1][/] [0][+][1][+][1][//]H1)). 3: astepr (([1][/] [0][+][1][+][1][//]H1)[^]n[*]([1][/] [0][+][1][+][1][//]H1)). 3: apply eq_reflexive. rstepl (([1][/] ([0][+][1][+][1])[^]n[//]nexp_resp_ap_zero n H1)[*]Two[*] ([1][/] [0][+][1][+][1][//]H1)). astepl (([1][/] ([0][+][1][+][1])[^]n[//]nexp_resp_ap_zero n H1)[*] (Two[*]([1][/] [0][+][1][+][1][//]H1))). rstepl (([1][/] ([0][+][1][+][1])[^]n[//]nexp_resp_ap_zero n H1)[*][1]). rstepl ([1][/] ([0][+][1][+][1])[^]n[//]nexp_resp_ap_zero n H1). astepl ((OneR[/] [0][+][1][+][1][//]H1)[^]n). apply eq_reflexive. astepr (([1][/] [0][+][1][+][1][//]H1)[^]S n). apply eq_reflexive. apply AbsIR_wd. rational. Qed.
imports: CoRN.metrics.ContFunctions