proposition: Lemma uniform_inde (M : probMonad real_realType) (A : Type) a (x : seq A) {B} (m : M B) : uniform a x >> m = m.
proof: Proof. elim: x m => [/= m|x xs IH m]; first by rewrite bindretf. by rewrite uniform_cons choice_bindDl IH bindretf 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) infotheo(Reals_ext)