proposition: Lemma convA' (r s : {prob R}) a b c : [p_of r, s] != 1%:pr -> a <| [p_of r, s] |> (b <| [q_of r, s] |> c) = (a <| r |> b) <| s |> c.
proof: Proof. move=> H; have [->|s0] := eqVneq s 0%:pr. - by rewrite p_of_r0 conv0 q_of_r0 conv0 conv0. - by rewrite convA s_of_pqK // r_of_pqK. 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