proposition: Lemma big_rV_prod n f (X : {set 'rV[A * B]_n}) : \big[M/idx]_(a in 'rV[A * B]_n | a \in X) f a = \big[M/idx]_(a in {: 'rV[A]_n * 'rV[B]_n} | (prod_rV a) \in X) f (prod_rV a).
proof: Proof. rewrite (reindex_onto (@rV_prod _ _ _) (@prod_rV _ _ _)) //=; last first. move=> ? _; by rewrite prod_rVK. apply eq_big => [?|? _]; by rewrite rV_prodK // eqxx andbC. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) logb ssr_ext ssralg_ext