proposition: Lemma distribute (x y z : A) (p q : {prob R}) : x <| p |> (y <| q |> z) = (x <| p |> y) <| q |> (x <| p |> z).
proof: Proof. by rewrite -{1}(convmm q x) convACA. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix fingroup perm) Reals Lra mathcomp(mathcomp_extra Rstruct reals) ssrR Reals_ext realType_ext Ranalysis_ext ssr_ext ssralg_ext logb fdist convex