proposition: Lemma uniform_cons (M : probMonad real_realType) (A : Type) (def : A) h s : uniform def (h :: s) = Ret h <| (/ IZR (Z_of_nat (size (h :: s))))%coqR%:pr |> uniform def s :> M A.
proof: Proof. by case: s => //=; rewrite (@choice_ext 1%:pr) // ?choice1 //= Rinv_1. 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)