proposition: Lemma coupling_self { A } (d : SDistr A) : coupling (coupling_self_SDistr d) d d.
proof: Proof. unfold coupling. unfold coupling_self_SDistr. split. - unfold lmg. unfold dmargin. apply distr_ext. move=> a. rewrite dlet_dlet. have coucou: d a = (\dlet_(y <- d) dunit y) a . rewrite dlet_dunit_id. reflexivity. rewrite coucou. f_equal. f_equal. apply boolp.funext. move=> y. apply distr_ext. move=> b. rewrite dlet_unit. reflexivity. - unfold rmg. unfold dmargin. apply distr_ext. move=> a. rewrite dlet_dlet. have coucou: d a = (\dlet_(y <- d) dunit y) a . rewrite dlet_dunit_id. reflexivity. rewrite coucou. f_equal. f_equal. apply boolp.funext. move=> y. apply distr_ext. move=> b. rewrite dlet_unit. reflexivity. Qed.
imports: Coq(RelationClasses Morphisms Utf8) Mon(SPropMonadicStructures SpecificationMonads MonadExamples SPropBase FiniteProbabilities) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum finmap.set finmap.finmap xfinmap) Crypt(Axioms ChoiceAsOrd SubDistr Couplings Theta_dens Theta_exCP LaxComp FreeProbProg RelativeMonadMorph_prod StateTransformingLaxMorph choice_type)