proposition: Lemma convACA (x1 y1 x2 y2 : A) p q : (x1 <|q|> y1) <|p|> (x2 <|q|> y2) = (x1 <|p|> x2) <|q|> (y1 <|p|> y2).
proof: Proof. have [->|p0] := eqVneq p 0%:pr; first by rewrite !conv0. have [->|q0] := eqVneq q 0%:pr; first by rewrite !conv0. have [->|p1] := eqVneq p 1%:pr; first by rewrite !conv1. have [->|q1] := eqVneq q 1%:pr; first by rewrite !conv1. set r := [p_of q, p]. have r1 : (r != 1%:pr)%coqR. by rewrite p_of_neq1//; apply/andP; split; rewrite -?prob_gt0 -?prob_lt1. rewrite -(convA' x1 y1) //. rewrite (convC _ y1). set s := [q_of q, p]. set t := (Prob.p (Prob.p s).~%:pr * Prob.p q)%:pr. have t1 : (Prob.p t < 1)%coqR. apply/RltP. rewrite -prob_lt1; apply/eqP => t1; subst t. have {q1} : (Prob.p q < 1)%coqR by apply/RltP; rewrite -prob_lt1. move/RltP. rewrite R1E. move/(congr1 (@Prob.p _)) : t1 => /= <-. move/RltP. rewrite -ltR_pdivr_mulr; last by apply/RltP; rewrite -prob_gt0. rewrite divRR // /onem ltR_subr_addl ltRNge; apply. by rewrite -{1}[in (1%R <= _)%coqR](add0R 1%R) leR_add2r. rewrite -(convA' x2); last by rewrite prob_lt1 p_of_rsC /= p_of_rsE; apply/RltP. rewrite -(convA' x1) //; last by rewrite p_of_rsC. rewrite (convC _ y2 y1) /=. congr (_ <| _ |> _); first by rewrite p_of_rsC. congr (_ <| _ |> _). apply val_inj => /=. rewrite /s /onem /= !(p_of_rsE,q_of_rsE) /= !(p_of_rsE,q_of_rsE) /= /onem. rewrite -!RminusE -R1E -!RmultE -!RinvE'. field. rewrite subR_eq0 mulRC; apply/nesym/eqP. by rewrite RmultE -p_of_rsE. congr (_ <| _ |> _). apply val_inj => /=. rewrite -[in RHS](onemK (Prob.p p)); congr onem. rewrite q_of_rsE {1}p_of_rsE /= q_of_rsE p_of_rsE /= /onem. rewrite -!RminusE -!R1E -!RmultE -!RinvE'. field. split. rewrite subR_eq0; apply/nesym/eqP; by rewrite RmultE -p_of_rsE. rewrite mulRBl mul1R subRBA subRK mulRDr mulR1 mulRN addR_opp subRBA subRK. rewrite subR_eq0 => /esym; exact/eqP. 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