proposition: Lemma d_is_lipschitz : forall a : X, lipschitz (projected_bin_fun X X IR_as_CPsMetricSpace (cms_d (c:=X)) a).
proof: Proof. intro a. red in |- *. simpl in |- *. exists 0. intros x y. astepr (OneR[*](x[-d]y)). astepr (x[-d]y). apply rev_tri_ineq'. Qed.
imports: CoRN.metrics.ContFunctions