proposition: Lemma Cmap2_comm : forall (X Y : MetricSpace) (Xpl : PrelengthSpace X) (f : ProductMS X X --> Y), (forall a b :X, msp_eq (f (a,b)) (f (b,a))) -> forall (a b:Complete X), @msp_eq (Complete Y) (uc_complete_curry (Cmap (ProductMS_prelength Xpl Xpl) f) a b) (uc_complete_curry (Cmap (ProductMS_prelength Xpl Xpl) f) b a).
proof: Proof. intros. assert (ucEq (Cmap (ProductMS_prelength Xpl Xpl) f) (Cmap (ProductMS_prelength Xpl Xpl) (uc_compose f (uc_flip X X)))). { intro x. apply Cmap_wd. apply ucEq_equiv. intros xy. simpl. rewrite H. destruct xy. reflexivity. reflexivity. } specialize (H0 (undistrib_Complete (a,b))). simpl in H0. simpl. intros e1 e2. specialize (H0 e1 e2). simpl. simpl in H0. assert (forall x, eq (QposInf_bind (λ e : Qpos, e) x) x). { intro x. destruct x;reflexivity. } rewrite H1 in H0. apply H0. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.metric2.Classification CoRN.metric2.UniformContinuity CoRN.metric2.Prelength CoRN.metric2.Complete CoRN.metric2.LocatedSubset Coq.Unicode.Utf8