proposition: Lemma coupling_vs_ret : d = SDistr_unit (F_choice_prod (npair A1 A2)) (a1,a2) <-> coupling d (SDistr_unit A1 a1) (SDistr_unit A2 a2).
proof: Proof. split. - intro dCoupl. unshelve eapply SDistr_unit_F_choice_prod_coupling. assumption. - intro dCoupl. unshelve eapply coupling_SDistr_unit_F_choice_prod. 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)