proposition: Lemma card_non_zero {F : finType} {w0 : F} : #|F|%:~R != 0 :> R.
proof: Proof. eapply fintype0 in w0 as h. apply /negP. intro n. eapply h. rewrite intr_eq0 in n. move: n => /eqP n. inversion n. reflexivity. Qed.
imports: Coq(Relation_Definitions RelationClasses Morphisms Utf8) Mon(FiniteProbabilities SPropMonadicStructures SpecificationMonads MonadExamples SPropBase) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum) Crypt(Axioms ChoiceAsOrd SubDistr Couplings Theta_dens Theta_exCP LaxComp FreeProbProg)