proposition: Lemma mpair_uniform_base_case (M : probMonad real_realType) (A : Type) a x (y : seq A) : (0 < size y)%nat -> uniform (a, a) (cp [:: x] y) = mpair (uniform a [:: x], uniform a y) :> M _.
proof: Proof. move=> y0; rewrite cp1. transitivity (@uniform M _ a y >>= (fun y' => Ret (x, y'))). by rewrite -(compE (uniform _)) (uniform_naturality a) // compE fmapE. transitivity (do z <- Ret x; do y' <- uniform a y; Ret (z, y') : M _)%Do. by rewrite bindretf. by []. 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)