proposition: Lemma coupling_vs_bind : coupling (SDistr_bind (F_choice_prod(npair A1 A2)) (F_choice_prod(npair B1 B2)) kd dA) (SDistr_bind A1 B1 f1 c1) (SDistr_bind A2 B2 f2 c2).
proof: Proof. split. - unfold lmg. unfold SDistr_bind. unfold dfst. move: dA_coup. rewrite /coupling /lmg. intros [H1 H2]. rewrite <- H1. unfold dfst. apply distr_ext. intro b. rewrite (dlet_dlet kd (fun x => dunit x.1) dA). rewrite (dlet_dlet _ _ dA). apply (@eq_in_dlet _ _ _). move => x12 Hsupp b2. destruct x12. simpl. rewrite (dlet_unit). assert (0 < dA (s, s0) = true). apply msupp. assumption. specialize (kd_pcoup s s0 H). unfold coupling in kd_pcoup. destruct kd_pcoup. unfold lmg in H0. unfold dfst in H0. rewrite H0. reflexivity. intro x. reflexivity. - unfold rmg. unfold SDistr_bind. unfold dfst. move: dA_coup. rewrite /coupling /lmg. intros [H1 H2]. rewrite <- H2. unfold dfst. apply distr_ext. intro b. rewrite (dlet_dlet kd (fun x => dunit x.2) dA). rewrite (dlet_dlet _ _ dA). apply (@eq_in_dlet _ _ _). move => x12 Hsupp b2. destruct x12. simpl. rewrite (dlet_unit). assert (0 < dA (s, s0) = true). apply msupp. assumption. specialize (kd_pcoup s s0 H). unfold coupling in kd_pcoup. destruct kd_pcoup. unfold rmg in H3. unfold dfst in H3. rewrite H3. reflexivity. intro x. reflexivity. 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)