proposition: Lemma convA0 (p q r s : {prob R}) a b c : Prob.p p = (Prob.p r * Prob.p s)%coqR :> R -> ((Prob.p s).~ = (Prob.p p).~ * (Prob.p q).~)%coqR -> a <| p |> (b <| q |> c) = (a <| r |> b) <| s |> c.
proof: Proof. move=> H1 H2. have [r0|r0] := eqVneq r 0%:pr. rewrite r0 conv0 (_ : p = 0%:pr) ?conv0; last first. by apply/val_inj; rewrite /= H1 r0 mul0R. congr (_ <| _ |> _); move: H2; rewrite H1 r0 mul0R onem0 mul1R. by move/(congr1 (@onem real_realType)); rewrite !onemK => ?; exact/val_inj. have [s0|s0] := eqVneq s 0%:pr. have p0 : p = 0%:pr by apply/val_inj; rewrite /= H1 s0 mulR0. rewrite s0 conv0 p0 // ?conv0. rewrite (_ : q = 0%:pr) ?conv0 //. move: H2; rewrite p0 onem0 mul1R => /(congr1 (@onem real_realType)); rewrite !onemK => sq. by rewrite -s0; exact/val_inj. rewrite convA; congr ((_ <| _ |> _) <| _ |> _). apply val_inj; rewrite /= s_of_pqE. move/(congr1 (@onem real_realType)) : H2. by rewrite onemK => ->. exact: (@r_of_pq_is_r _ _ _ _ s). 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