proposition: Lemma uniform_nseq (M : probMonad real_realType) (A : Type) (def : A) h n : uniform def (nseq n.+1 h) = Ret h :> M A.
proof: Proof. elim: n => // n IH. by rewrite (_ : nseq _ _ = h :: nseq n.+1 h) // uniform_cons IH choicemm. 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)