proposition: Lemma CoupleCorrect1 : forall p, msp_eq (Couple ((Cfst p), (Csnd p))) p.
proof: Proof. intros p e1 e2. rewrite Qplus_0_r. destruct (regFun_prf p e1 e2). split; simpl; auto. Qed.
imports: CoRN.metric2.ProductMetric CoRN.metric2.Complete