proposition: Lemma aux_lemma { A } {d : SDistr A} : forall a1 a2, 0 < (coupling_self_SDistr d) (a1,a2) -> a1 = a2.
proof: Proof. move=> a1 a2. unfold coupling_self_SDistr. rewrite dmargin_psumE. move=> Hpsum. have Hpsum' : psum (fun x : A => ((x, x) == (a1, a2))%:R * d x) <> 0. move=> abs. rewrite -abs in Hpsum. rewrite Order.POrderTheory.ltxx in Hpsum. discriminate. clear Hpsum. eapply neq0_psum in Hpsum'. destruct Hpsum'. apply aux_domain in H. destruct (eqType_lem bool_eqType ((x,x) == (a1,a2)) true) as [Houi | Hnon]. move: Houi => /eqP Houi. move: Houi => [H1 H2]. rewrite -H1 -H2. reflexivity. have Hnon' : (x,x) == (a1,a2) = false. destruct ((x,x) == (a1,a2)). contradiction. reflexivity. rewrite Hnon' in H. cbn in H. contradiction. 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)