proposition: Lemma dsub'_is_lipschitz : forall (y : M) (x1 x2 : SubMetricSpace M P), C[*]dIR (dsub' M P y x1) (dsub' M P y x2)[<=]C[*](dsub M P x1 x2).
proof: Proof. intros. apply mult_resp_leEq_lft. 2: apply less_leEq. 2: apply constant_positive. unfold dsub'. unfold dsub. case x1. case x2. intros. simpl. astepl (dIR (y[-d]scs_elem0) (y[-d]scs_elem)). apply rev_tri_ineq'. unfold dIR. apply ABSIR_wd. assert ((y[-d]scs_elem0)[=](scs_elem0[-d]y)). apply ax_d_com. apply CPsMetricSpace_is_CPsMetricSpace. assert ((y[-d]scs_elem)[=](scs_elem[-d]y)). apply ax_d_com. apply CPsMetricSpace_is_CPsMetricSpace. algebra. Qed.
imports: CoRN.metrics.ContFunctions CoRN.metrics.CMetricSpaces CoRN.metrics.CPMSTheory