proposition: Lemma coinarb_spec p : coinarb p = arb.
proof: Proof. rewrite /coinarb /bcoin. rewrite choice_bindDl. rewrite !bindretf. rewrite /arb !alt_bindDl !bindretf eqxx. by rewrite eq_sym altC choicemm. 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)