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