proposition: Lemma bcoin13E_pair {M : probMonad real_realType} def (f : bool -> M bool) : uniform (def, def) (cp (enum X) (enum X)) >>= (fun hp => f (hp.1 == hp.2)) = bcoin (/ 3)%coqR%:pr >>= f.
proof: Proof. transitivity (uniform (def, def) (cp (enum X) (enum X)) >>= (fun hp => Ret (hp.1 == hp.2) >>= f)). bind_ext => -[h p] /=; by rewrite bindretf. rewrite -bindA uniform_unfold_pair !eqxx. rewrite (negbTE a_neq_c). rewrite (eq_sym b) (negbTE a_neq_b). rewrite (negbTE b_neq_c). rewrite 2!(eq_sym c) (negbTE a_neq_c). rewrite (negbTE b_neq_c). by rewrite choiceA_compute /= -uFFTE. Qed.
imports: Reals Lra mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra reals Rstruct) infotheo(ssrR realType_ext Reals_ext proba) monae_lib hierarchy monad_lib fail_lib proba_lib