proposition: Lemma psum_SDistr_unit : psum (SDistr_unit A a) = 1.
proof: Proof. rewrite (@psum_finseq R A (SDistr_unit A a) [::a]). rewrite big_cons big_nil. rewrite GRing.addr0. unfold SDistr_unit. rewrite dunit1E. rewrite refl_true. simpl. rewrite normr1. reflexivity. rewrite cons_uniq. apply /andP. split. trivial. trivial. unfold sub_mem. intro x. unfold in_mem. simpl. rewrite dunit1E. intro Hx. apply /orP. left. move: Hx => /eqP. destruct (eqType_lem A a x). intro Hx. apply /eqP. symmetry ; assumption. assert (a == x = false). apply Bool.not_true_is_false. intro Hax. unshelve eapply elimT in Hax. exact (a = x). contradiction. apply eqP. rewrite H0. simpl. intro H1. epose (H2 := H1 _). contradiction. Unshelve. reflexivity. 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)