proposition: Lemma bcoin23E_pair {M : probMonad real_realType} def : uniform (def, def) (cp (enum X) (enum X)) >>= (fun hp => Ret (hp.1 != hp.2)) = bcoin (/ 3)%coqR.~%:pr :> M _.
proof: Proof. pose P := fun a b : X => a != b. transitivity (uniform (def, def) (cp (enum X) (enum X)) >>= (fun hp => Ret (P hp.1 hp.2)) : M _). by bind_ext. rewrite uniform_unfold_pair {}/P !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 /= -uTTFE. 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