proposition: Lemma enum_prodE {T1 T2 : finType} : enum [finType of T1 * T2] = prod_enum T1 T2.
proof: Proof. by rewrite enumT Finite.EnumDef.enumDef. Qed.
imports: Reals mathcomp(all_ssreflect all_algebra vector reals classical_sets Rstruct) infotheo(convex)