proposition: Lemma size_prod_seq_eq1 (I : eqType) (s : seq I) (P : pred I) (F : I -> {poly R}) : reflect (forall i, P i && (i \in s) -> size (F i) = 1) (size (\prod_(i <- s | P i) F i) == 1%N).
proof: Proof. rewrite (big_morph _ (id1:=true) size_mul_eq1) ?size_polyC ?oner_neq0//. rewrite big_all_cond; apply/(iffP allP). by move=> h i /andP[Pi ins]; apply/eqP/(implyP (h i ins) Pi). by move=> h i ins; apply/implyP => Pi; rewrite h ?Pi. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)