proposition: Lemma psum_coupling_right : psum d = psum c2.
proof: Proof. rewrite (@psum_pair_swap R A1 A2 d). f_equal. destruct hCoupl as [lH rH]. rewrite -rH. unfold rmg. apply boolp.funext. intro x2. rewrite dsndE. reflexivity. destruct d as [dd d2 d3 d4]. simpl. assumption. Qed.
imports: Mon(FiniteProbabilities SPropMonadicStructures SpecificationMonads MonadExamples SPropBase FiniteProbabilities) Coq(RelationClasses Morphisms) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity) mathcomp(all_ssreflect all_algebra reals distr realsum) Crypt(Axioms ChoiceAsOrd only_prob.SubDistr)