proposition: Corollary arb_spec_convexity p : arb = (arb : M _) [~] bcoin p.
proof: Proof. exact: alt_absorbs_choice. 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)