proposition: Lemma convDr (x y z : T) (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: HB(structures) mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets Rstruct) mathcomp(ssrnum ereal) mathcomp(lra Rstruct reals) Reals ssrR Reals_ext Ranalysis_ext ssr_ext ssralg_ext logb realType_ext fdist