proposition: Lemma index_allpairs {T1 T2: eqType} (s1: seq T1) (s2: seq T2) x1 x2 : x1 \in s1 -> x2 \in s2 -> index (x1, x2) [seq (x1, x2) | x1 <- s1, x2 <- s2] = ((index x1 s1) * (size s2) + index x2 s2)%N.
proof: Proof. move=>ins1 ins2. elim: s1 ins1=>//= a s1 IHs1 ins1. rewrite index_cat. case ax: (a == x1). move: ax=>/eqP ax; subst a; rewrite /muln /muln_rec /addn /addn_rec /=. move: ins2=>/(map_f (fun x => (x1, x))) ->. by apply index_map=> x y eq; inversion eq. move: ins1; rewrite in_cons=>/orP; case=> [ /eqP xa | ins1 ]. by subst a; move: ax; rewrite eq_refl. case in12: ((x1, x2) \in [seq (a, x0) | x0 <- s2]). by move: in12=>/mapP [x xin xeq]; inversion xeq; subst a; move: ax; rewrite eq_refl. by rewrite size_map (IHs1 ins1) addnA. Qed.
imports: Reals mathcomp(all_ssreflect all_algebra vector reals classical_sets Rstruct) infotheo(convex)