proposition: Lemma is_uniform {F : finType} (w0 : F) : isdistr (fun w : F => (@r F w0)).
proof: Proof. split. - move => w; apply: r_nonneg. - move => J uniq_J. apply /idP. apply: le_trans. -- by apply: (cardinality_bound J uniq_J r r_nonneg). -- rewrite /r -GRing.invf_div GRing.divr1 GRing.divff. by []. exact (@card_non_zero F w0). 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)