proposition: Lemma convACA' (a b c d : T) (p q r : {prob R}) : exists p' q' r', (a <|p|> b) <|q|> (c <|r|> d) = (a <|p'|> c) <|q'|> (b <|r'|> d).
proof: Proof. rewrite (convC p) convA convC !convA. set C0 := _.~%:pr. set C1 := _.~%:pr. rewrite -convA' (convC _ d) convC. by eexists; eexists; eexists; congr ((_ <|_|> _) <|_|> (_ <|_|> _)). 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