proposition: Lemma translate_ident : forall x:CR, (translate 0 x==x)%CR.
proof: Proof. intros x. unfold translate. assert (H:msp_eq (Qtranslate_uc 0) (uc_id _)). apply ucEq_equiv. intros a. simpl. rewrite Qplus_0_l. reflexivity. simpl. intros e1 e2. destruct x; simpl. rewrite Qplus_0_r. rewrite Qplus_0_l. apply regFun_prf. Qed.
imports: QArith Qabs CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.metric2.CRmetric CoRN.model.totalorder.QMinMax CoRN.model.metric2.Qmetric CoRN.metric2.ProductMetric CoRN.stdlib_omissions.Pair MathClasses.interfaces.canonical_names