proposition: Lemma uTTFE (M : probMonad real_realType) : uTTF = bcoin (/ 3).~%:pr :> M _.
proof: Proof. rewrite /uTTF /bcoin uniform_cons. rewrite (_ : _%:pr = (/ 3)%:pr)%R; last exact/val_inj. rewrite uniform_cons. rewrite [in X in _ <| _ |> X](_ : _%:pr = (/ 2)%:pr)%R; last exact/val_inj. rewrite uniform_singl //=. rewrite (@choiceA_alternative _ _ _ _ _ (/ 2)%:pr (/ 3).~%:pr) ?choicemm //. rewrite /= /onem; split. rewrite -RmultE -RminusE -R1E. field. rewrite -!RminusE -RmultE -R1E. field. 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)