proposition: Lemma binconvA p q a b c : a <& p &> (b <& q &> c) = (a <& [r_of p, q] &> b) <& [s_of p, q] &> c.
proof: Proof. rewrite /binconv. set g := fun i : 'I_3 => if i <= 0 then a else if i <= 1 then b else c. rewrite [X in <&>_(fdistI2 q) X](_ : _ = g \o lift ord0); last first. by apply funext => i; case/orP: (ord2 i) => /eqP ->. rewrite [X in <&>_(_ [r_of p, q]) X](_ : _ = g \o (widen_ord (leqnSn 2))); last first. by apply funext => i; case/orP: (ord2 i) => /eqP ->. rewrite 2!axmap. set d1 := fdistmap _ _. set d2 := fdistmap _ _. set ord23 := Ordinal (ltnSn 2). have -> : a = g ord0 by []. have -> : c = g ord23 by []. rewrite -2!axproj 2!convn_if 2!axbary. congr (<&>_ _ _); apply fdist_ext => j. rewrite !fdist_convnE !big_ord_recl !big_ord0 /=. rewrite !fdistI2E !fdistmapE !fdist1E !addr0 /=. case: j => -[|[|[]]] //= Hj. - rewrite [in RHS](big_pred1 ord0)// big1; last by move=> [] []. by rewrite fdistI2E eqxx !(mulr0,addr0) mulr1 mulrC -p_is_rs. - rewrite (big_pred1 ord0) // (big_pred1 (Ordinal (ltnSn 1))) //. rewrite !fdistI2E !eqxx !(mulr0,addr0,add0r)/=. rewrite {2}/onem mulrDr mulr1 mulrN [in RHS]GRing.mulrC. rewrite -p_is_rs s_of_pqE onemM !onemK /onem mulrBl mul1r. by rewrite -!addrA (addrC (Prob.p p)) !addrA subrK. - rewrite (big_pred1 (Ordinal (ltnSn 1))) //. rewrite big1; last by case => -[|[]]. by rewrite !fdistI2E 2!mulr0 2!add0r mulr1 s_of_pqE onemK. 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