proposition: Lemma plus_resp_lipschitz : forall (X : CPsMetricSpace) (f g : CSetoid_fun X IR_as_CPsMetricSpace) (H : lipschitz f) (H1 : lipschitz g), lipschitz (compose_CSetoid_bin_fun X IR_as_CPsMetricSpace IR_as_CPsMetricSpace f g (csg_op (c:=IR))).
proof: Proof. red in |- *. unfold lipschitz in |- *. intros X f g H H1. elim H. intros x H2. elim H1. intros x0 H3. exists (Nat.max x x0 + 1). intros x1 y. astepl (dIR (f x1[+]g x1) (f y[+]g y)). unfold dIR in |- *. unfold dIR in |- *. astepl (ABSIR (g x1[-]g y[+](f x1[-]f y))). apply leEq_transitive with (ABSIR (g x1[-]g y)[+]ABSIR (f x1[-]f y)). apply IR_tri_ineq. apply leEq_transitive with ((Two:IR)[^]x0[*](x1[-d]y)[+]ABSIR (f x1[-]f y)). apply plus_resp_leEq. astepl (g x1[-d]g y). apply H3. apply leEq_transitive with (Two[^]x0[*](x1[-d]y)[+]Two[^]x[*](x1[-d]y)). apply plus_resp_leEq_lft. astepl (f x1[-d]f y). apply H2. astepr ((Two:IR)[*]Two[^]Nat.max x x0[*](x1[-d]y)). apply leEq_transitive with (Two[^]Nat.max x x0[*](x1[-d]y)[+]Two[^]Nat.max x x0[*](x1[-d]y)). apply plus_resp_leEq_both. apply mult_resp_leEq_rht. apply great_nexp_resp_le. apply less_leEq. apply one_less_two. intuition. apply ax_d_nneg. apply CPsMetricSpace_is_CPsMetricSpace. apply mult_resp_leEq_rht. apply great_nexp_resp_le. apply less_leEq. apply one_less_two. intuition. apply ax_d_nneg. apply CPsMetricSpace_is_CPsMetricSpace. apply eq_imp_leEq. rational. astepl (Two[^]1[*]Two[^]Nat.max x x0[*](x1[-d]y)). 2: apply AbsIR_wd. apply mult_wdl. astepl ((Two:IR)[^](Nat.max x x0 + 1)). 2: astepl ((Two:IR)[^]Nat.max x x0[*]Two[^]1). 2: apply mult_commutes. astepr ((Two:IR)[^](Nat.max x x0 + 1)). rational. rational. Qed.
imports: CoRN.metrics.ContFunctions