proposition: Lemma eqType_lem : forall (Z : eqType) (z t : Z), z = t \/ ~(z = t).
proof: Proof. intros Z z t. case Hzt : (z==t). left. move: Hzt => /eqP. trivial. right. move: Hzt => /eqP. trivial. 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)