proposition: Lemma coinarb_spec_convexity p w : coinarb p = (bcoin w : M _) [~] (Ret false : M _) [~] (Ret true : M _) [~] bcoin (Prob.p w).~%:pr.
proof: Proof. rewrite coinarb_spec [in LHS]/arb [in LHS](convexity _ _ w) 2!choicemm. rewrite -/(bcoin w) -altA altCA -!altA; congr (_ [~] _). rewrite altA altC; congr (_ [~] (_ [~] _)). by rewrite choiceC. 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)