proposition: Lemma choiceACA {M : probMonad real_realType} T q p : @interchange (prob_convType M T) (fun a b => a <|p|> b) (fun a b => a <|q|> b).
proof: Proof. by move=> *; exact: convACA. 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)