proposition: Lemma size_prod_eq1 (I : finType) (P : pred I) (F : I -> {poly R}) : reflect (forall i, P i -> size (F i) = 1) (size (\prod_(i | P i) F i) == 1).
proof: Proof. apply: (iffP (size_prod_seq_eq1 _ _ _)) => Hi i. by move=> Pi; apply: Hi; rewrite Pi /= mem_index_enum. by rewrite mem_index_enum andbT; apply: Hi. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)