proposition: Lemma uniform_naturality (M : probMonad real_realType) (A B : Type) (a : A) (b : B) (f : A -> B) : forall x, (0 < size x)%nat -> ((@uniform M _ b) \o map f) x = ((M # f) \o uniform a) x.
proof: Proof. elim=> // x [_ _|x' xs]; first by rewrite [in RHS]compE fmapE bindretf. move/(_ isT) => IH _. rewrite compE [in RHS]compE [in LHS]uniform_cons [in RHS]uniform_cons. set p := (@Prob.mk _ (/ IZR (Z.of_nat (size _)))%coqR _ in X in _ = X). rewrite (_ : @Prob.mk _ (/ _)%coqR _ = p); last first. by apply val_inj; rewrite /= size_map. move: IH; rewrite 2!compE => ->. by rewrite [in RHS]fmapE choice_bindDl bindretf fmapE. Qed.
imports: HB(structures) Reals Lra mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals mathcomp_extra Rstruct lra) infotheo(ssrR realType_ext Reals_ext) infotheo(proba convex necset) monae_lib hierarchy monad_lib fail_lib infotheo(fdist) mathcomp(reals Rstruct) infotheo(Reals_ext)