fact: Fixpoint uniform {M : probMonad real_realType} {A : Type} (def : A) (s : seq A) : M A := match s with | [::] => Ret def | [:: x] => Ret x | x :: xs => Ret x <| (/ IZR (Z_of_nat (size (x :: xs))))%coqR%:pr |> uniform def xs end.
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)