proposition: Lemma distr_ext : forall (A : choiceType) (mu nu : {distr A/R}), distr.mu mu =1 distr.mu nu -> mu = nu.
proof: Proof. move=> A [mu muz mu_smbl mu_psum] [nu nuz nu_smbl nu_psum]. simpl. intro H. move: muz mu_smbl mu_psum nuz nu_smbl nu_psum. apply boolp.funext in H. rewrite H. intuition. f_equal. all: apply proof_irrelevance. Qed.
imports: Coq(Relation_Definitions Morphisms) mathcomp(all_ssreflect all_algebra distr reals realsum) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) Crypt(ChoiceAsOrd Axioms)