proposition: Lemma Uniform_F_is_uniform_F { i : Index } : get_d (@Uniform_F i) = (@uniform_F (fin_family i) (F_w0 i)).
proof: Proof. cbn. apply: distr_ext. cbn. rewrite /SDistr_bind /Uniform_F /SDistr_unit => w. rewrite (@dlet_dunit_id _ _ (mkdistrd (fun=> r)) w) /mkdistrd. destruct idP. + by []. + exfalso. apply n. rewrite /boolp.asbool //=. case (boolp.pselect (isdistr (fun=> r))); intuition. exfalso. apply n0. apply: (@is_uniform (fin_family i) (F_w0 i)). Qed.
imports: Coq(RelationClasses Morphisms) 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 RulesProb UniformDistrLemmas choice_type Prelude)