proposition: Lemma id_is_lipschitz : forall X : CPsMetricSpace, lipschitz (id_un_op X).
proof: Proof. intro X. red in |- *. simpl in |- *. exists 0. intros x y. astepr (OneR[*](x[-d]y)). astepr (x[-d]y). apply leEq_reflexive. Qed.
imports: CoRN.metrics.CPseudoMSpaces