proposition: Lemma aux_lemma0 {A} (c : SDistr A) (a1 a2 : A) : coupling_self_SDistr c (a1,a2) = (if a1 == a2 then c a1 else 0).
proof: Proof. destruct (eqType_lem A a1 a2). - rewrite H. unfold coupling_self_SDistr. rewrite refl_true. unfold dmargin. have coucou : c a2 = (\dlet_(x <- c) dunit x) a2. symmetry. rewrite dlet_dunit_id. reflexivity. rewrite coucou. f_equal. Abort. Lemma aux_domain : forall u v : R, u * v <> 0 -> u <> 0. Proof. move=> u v. apply contra_not. move=> H0. rewrite H0. apply GRing.Theory.mul0r. 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)