proposition: Lemma nth_allpairs [T1 T2 rT : Type] (f : T1 -> T2 -> rT) (s1: seq T1) (s2: seq T2) (x1: T1) (x2: T2) (x: rT) (i: 'I_(size s1 * size s2)) : nth x (allpairs f s1 s2) i = let (i, j) := split_prod i in f (nth x1 s1 i) (nth x2 s2 j).
proof: Proof. elim: s1 i=>/= [| a s1 IHs1] i. by exfalso; move: i=>[i ilt]; move: ilt; rewrite /muln /muln_rec /= ltn0. move: i; rewrite /muln /muln_rec /= -/muln_rec -/muln -/addn_rec -/addn. have->: (size s2 + size s1 * size s2 = size (map (f a) s2) + size (allpairs f s1 s2))%N. rewrite size_map. by move: (allpairs_tupleP f (in_tuple s1) (in_tuple s2))=>/eqP->. move=>i; rewrite nth_cat_ord. rewrite -{2 3}[i]splitK. rewrite /split; case: ltnP=>/= i0. rewrite (set_nth_default (f a x2)) //. case: i i0=> [i ilt'] /=; rewrite size_map=> ilt. by rewrite (nth_map x2)// divn_small// modn_small. move: i i0; rewrite size_map=> [[i ilt']] i0. have ilt: ((i - size s2) < size s1 * size s2)%N. move: (allpairs_tupleP f (in_tuple s1) (in_tuple s2))=>/eqP<-. apply (split_subproof i0). rewrite (IHs1 (Ordinal ilt))=> /=. rewrite addnC divnDr// divnn/= modnDr. have [s20|] := ltnP 0 (size s2); first by rewrite addn1. rewrite leqn0 => /eqP s20. by move: ilt; rewrite s20 muln0. Qed.
imports: Reals mathcomp(all_ssreflect all_algebra vector reals classical_sets Rstruct) infotheo(convex)