proposition: Lemma mpair_uniform (M : probMonad real_realType) (A : Type) a (x y : seq A) : (0 < size x)%nat -> (0 < size y)%nat -> mpair (uniform a x, uniform a y) = uniform (a, a) (cp x y) :> M (A * A)%type.
proof: Proof. elim: x y => // x; case=> [_ y _ size_y|x' xs IH y _ size_y]; apply/esym. exact/mpair_uniform_base_case. set xxs := x' :: xs. rewrite /cp -cat1s allpairs_cat -/(cp _ _) cp1 uniform_cat. pose n := size y. pose l := size (cp xxs y). rewrite (_ : size _ = n); last by rewrite size_map. rewrite (_ : Prob.mk _ = probdivRnnm n l); last first. by rewrite -/(cp _ _) -/l; exact/val_inj. pose m := size xxs. have lmn : (l = m * n)%nat by rewrite /l /m /n size_allpairs. rewrite (_ : probdivRnnm _ _ = @Prob.mk _ (/ (1 + m)%:R) (prob_invn _))%coqR; last first. apply val_inj => /=. rewrite lmn /divRnnm -mulSn mult_INR {1}/Rdiv Rinv_mult. rewrite mulRC -mulRA mulVR; last by rewrite INR_eq0' -lt0n. by rewrite mulR1 -addn1 addnC. rewrite -IH //. rewrite -/xxs. move: (@mpair_uniform_base_case M _ a x _ size_y). rewrite {1}/cp [in X in uniform _ X]/= cats0 => ->. rewrite -choice_bindDl. rewrite [in RHS]/mpair uniform_cat. rewrite [in RHS](_ : Prob.mk _ = probinvn m) //. by apply val_inj; rewrite /= /divRnnm div1R. 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)