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