proposition: Lemma uFFTE (M : probMonad real_realType) : uFFT = bcoin (/ 3)%:pr :> M _.
proof: Proof. rewrite /uFFT /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); last first. rewrite /= /onem; split. rewrite -RmultE -RminusE -R1E; field. rewrite -!RmultE -!RminusE -R1E; field. rewrite choicemm choiceC; congr (Ret true <| _ |> Ret false). by apply val_inj; rewrite /= onemK. 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)