proposition: Lemma two_coinsE : two_coins = two_coins'.
proof: Proof. rewrite /two_coins /two_coins' /bcoin. rewrite ![in LHS](choice_bindDl,bindretf). rewrite -choiceACA. by rewrite ![in RHS](choice_bindDl,bindretf). 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)