proposition: Lemma SDistr_unit_F_choice_prod_coupling : d = SDistr_unit (F_choice_prod (npair A1 A2)) (a1,a2) -> coupling d (SDistr_unit A1 a1) (SDistr_unit A2 a2).
proof: Proof. intro Hunit. split. - pose (retComm := @dmargin_dunit R (F_choice_prod (npair A1 A2)) A1 (a1,a2) fst). unfold lmg. rewrite Hunit. unfold SDistr_unit. simpl. apply distr_ext. assumption. - pose (retComm := @dmargin_dunit R (F_choice_prod (npair A1 A2)) A2 (a1,a2) snd). unfold rmg. rewrite Hunit. unfold SDistr_unit. simpl. apply distr_ext. 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)