proposition: Lemma distr_get : forall {A : Type} {chA : Choice.class_of A} x y, 0 < SDistr_unit (Choice.Pack chA) x y -> x = y.
proof: Proof. intuition. rewrite /SDistr_unit in H. rewrite dunit1E in H. case Hxy: (x==y). move: Hxy => /eqP Hxy //=. rewrite Hxy /= in H. rewrite (ltxx 0) in H. discriminate. Qed.
imports: mathcomp(all_ssreflect all_algebra boolp distr reals realsum) Mon(SpecificationMonads SPropBase SPropMonadicStructures) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) Crypt(ChoiceAsOrd SubDistr Couplings Axioms)