proposition: Lemma CRplus_uncurry_eq : forall x y : CR, msp_eq (CRplus x y) (Cmap (ProductMS_prelength QPrelengthSpace QPrelengthSpace) Qplus_uncurry (undistrib_Complete (x,y))).
proof: Proof. intros x y. unfold CRplus, ucFun2, CRplus_uc. transitivity (Cmap2 QPrelengthSpace QPrelengthSpace (uc_curry Qplus_uncurry) x y). 2: apply Cmap2_curry. apply Cap_wd. 2: reflexivity. apply Cmap_wd. 2: reflexivity. apply ucEq_equiv. split. apply Qle_refl. intros a. reflexivity. 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