proposition: Lemma lmg_SDistr_unit : lmg d = SDistr_unit A1 a1 -> forall (x1 : A1) (x2 : A2), ~(a1 = x1) -> d(x1,x2) = 0.
proof: Proof. intro rHcoupl. intros x1 x2. intro Hxa. unfold lmg in rHcoupl. unfold SDistr_unit in rHcoupl. assert (rHcoupl1 : dfst d x1 = dunit (T:=A1) a1 x1). rewrite rHcoupl. reflexivity. rewrite (dfstE d x1) (dunit1E a1 x1) in rHcoupl1. assert ((a1==x1 = false)). apply /eqP. assumption. rewrite H /= in rHcoupl1. epose (bla := eq0_psum _ rHcoupl1 x2). apply bla. Unshelve. eapply summable_fst. 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)