proposition: Lemma arbcoin_spec_convexity (p q : {prob real_realType}) : Prob.p p < Prob.p q < (Prob.p p).~ -> arbcoin p = (bcoin p : M _) [~] bcoin (Prob.p p).~%:pr [~] bcoin q.
proof: Proof. move=> H. rewrite arbcoin_spec !alt_lub. rewrite {1}(@lub_absorbs_conv [the semiLattConvType of altProb_semiLattConvType M bool] _ _ (magnified_weight H)). by rewrite magnify_conv. 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)