fact: Definition choiceA_real_realType (p q : {prob real_realType}) (a b c : M A) : let conv := (fun p (a b : choice_of_Type (M A)) => choice p A a b) in conv p a (conv q b c) = conv [s_of p, q] (conv [r_of p, q] a b) c.
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)