proposition: Lemma uniform_cat (M : probMonad real_realType) (A : Type) (a : A) s t : let m := size s in let n := size t in uniform a (s ++ t) = uniform a s <| (divRnnm m n)%:pr |> uniform a t :> M _.
proof: Proof. elim: s t => [t m n|s1 s2 IH t m n]. rewrite cat0s uniform_nil /= [X in _ <| X |> _](_ : _ = 0%:pr) ?choice0 //. by apply val_inj; rewrite /= /divRnnm div0R. case/boolP : (m.-1 + n == 0)%nat => [{IH}|] m1n0. have s20 : s2 = [::] by move: m1n0; rewrite {}/m /=; case: s2. have t0 : t = [::] by move: m1n0; rewrite {}/n /= addnC; case: t. subst s2 t. rewrite cats0 (_ : Prob.mk _ = 1%:pr) ?choice1 //. by apply val_inj; rewrite /= /divRnnm div1R invR1. rewrite cat_cons uniform_cons uniform_cons. set pv := ((/ _)%coqR). set v : {prob real_realType} := @Prob.mk _ pv _. set u := @Prob.mk_ _ ((size s2)%:R / (size s2 + size t)%:R)%coqR (prob_divRnnm_subproof _ _). rewrite -[RHS](@choiceA_alternative _ _ _ v u). by rewrite IH. rewrite -RmultE. split. rewrite 3!probpK -INR_IZR_INZ. rewrite (_ : INR _ = INR m) // mulRA mulVR; last by rewrite INR_eq0'. by rewrite mul1R /pv -INR_IZR_INZ [size _]/= size_cat -addSn. rewrite 3!probpK. transitivity ( (1 - 1 / INR (m + n)) * (1 - INR (m.-1) / INR (m.-1 + n)))%coqR; last first. congr (_ .~ * _)%R. by rewrite /v /pv probpK INR_IZR_INZ [size _]/= size_cat -addSn div1R. transitivity (INR n / INR (m + n))%coqR. rewrite {1}/onem -RminusE -R1E -{1}(Rinv_r (INR (m+n))); last exact/not_0_INR. rewrite -mulRBl -minus_INR; last by apply/leP; rewrite leq_addr. by rewrite minusE addnC addnK. rewrite {1}/Rdiv mulRC. rewrite {1}/Rdiv -[in LHS](mul1R (INR n)). rewrite -{1}(mulRV (INR (m.-1 + n))); last by rewrite INR_eq0'. rewrite 2!mulRA -(mulRA (_ * _)%coqR); congr Rmult. rewrite mulRC -subn1. rewrite addnC addnBA // minus_INR; last by apply/leP; rewrite addn_gt0 orbT. rewrite -/(_ / INR (m + n))%coqR. rewrite Rdiv_minus_distr {1}/Rdiv addnC Rinv_r //; exact/not_0_INR. rewrite -{1}(Rinv_r (INR (m.-1 + n))); last exact/not_0_INR/eqP. rewrite -Rdiv_minus_distr mulRC; congr (_ * _)%R. rewrite -minus_INR; last by apply/leP; rewrite leq_addr. by rewrite addnC minusE -subnBA // subnn subn0. 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)