proposition: Lemma arbcoin_spec p : arbcoin p = (bcoin p : M _) [~] bcoin (Prob.p p).~%:pr.
proof: Proof. rewrite /arbcoin /arb alt_bindDl 2!bindretf bindmret; congr (_ [~] _). by rewrite /bcoin choiceC choice_bindDl 2!bindretf eqxx. 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)