proposition: Lemma binconvC p a b : a <& p &> b = b <& ((Prob.p p).~)%:pr &> a.
proof: Proof. rewrite /binconv. set g1 := fun x => _. set g2 := fun x => _. have -> : g1 = g2 \o tperm ord0 (Ordinal (erefl (1 < 2))). rewrite /g1 /g2 /=. apply funext => i /=. by case/orP: (ord2 i) => /eqP -> /=; rewrite (tpermL,tpermR). rewrite axmap. congr (<&>_ _ _); apply fdist_ext => i. rewrite fdistmapE (bigD1 (tperm ord0 (Ordinal (erefl (1 < 2))) i)) /=; last first. by rewrite !inE tpermK. rewrite big1 ?addr0. rewrite !fdistI2E onemK. by case/orP: (ord2 i) => /eqP -> /=; rewrite (tpermL,tpermR). by move=> j /andP[] /eqP <-; rewrite tpermK eqxx. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets) Reals mathcomp(Rstruct reals) ssrR Reals_ext realType_ext Ranalysis_ext ssr_ext ssralg_ext fdist jfdist_cond fsdist convex