proposition: Lemma comp_resp_lipschitz : lipschitz f -> lipschitz g -> lipschitz (compose_CSetoid_fun X B C f g).
proof: Proof. unfold lipschitz in |- *. intros H H0. elim H. intros x H1. elim H0. intros x0 H2. exists (x + x0). simpl in |- *. intros x1 y. apply leEq_transitive with ((Two:IR)[^]x0[*](f x1[-d]f y)). apply H2. astepr (Two[^](x + x0)[*](x1[-d]y)). astepr (Two[^]x[*]Two[^]x0[*](x1[-d]y)). astepr (Two[^]x0[*]Two[^]x[*](x1[-d]y)). rstepr (Two[^]x0[*](Two[^]x[*](x1[-d]y))). apply mult_resp_leEq_lft. apply H1. apply nexp_resp_nonneg. apply less_leEq. apply pos_two. Qed.
imports: CoRN.metrics.CPseudoMSpaces