proposition: Lemma enum_rank_prod {T T': finType} i j : (nat_of_ord (@enum_rank [finType of T * T'] (i, j)) = (enum_rank i) * #|T'| + enum_rank j)%N.
proof: Proof. do 3 rewrite enum_rank_index. rewrite enumT Finite.EnumDef.enumDef cardE=>/=. by apply index_allpairs; rewrite enumT. Qed.
imports: Reals mathcomp(all_ssreflect all_algebra vector reals classical_sets Rstruct) infotheo(convex)