proposition: Lemma uniform_notin (M : probMonad real_realType) (A : eqType) (def : A) (s : seq A) B (ma mb : A -> M B) (p : pred A) : s != [::] -> (forall x, x \in s -> ~~ p x) -> uniform def s >>= (fun t => if p t then ma t else mb t) = uniform def s >>= mb.
proof: Proof. elim: s => [//|h t IH _ H]. rewrite uniform_cons. case/boolP : (t == [::]) => [/eqP -> {IH}|t0]. rewrite uniform_nil. rewrite (_ : _%:pr = 1%:pr); last by apply val_inj; rewrite /= Rinv_1. rewrite choice1. rewrite 2!bindretf ifF //; apply/negbTE/H; by rewrite mem_head. rewrite 2!choice_bindDl; congr (_ <| _ |> _). rewrite 2!bindretf ifF //; apply/negbTE/H; by rewrite mem_head. by rewrite IH // => a ta; rewrite H // in_cons ta orbT. 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)