proposition: Lemma natr_prod_eq1 (I : finType) (P : pred I) (F : I -> R) : (forall i, P i -> F i \is a nat_num) -> \prod_(i | P i) F i = 1 -> forall i, P i -> F i = 1.
proof: Proof. move=> natF /eqP; rewrite -prod_truncK// -[1]/1%:R eqr_nat prod_nat_seq_eq1. move/allP => a i Pi; apply/eqP; rewrite -[F i]truncK ?natF// eqr_nat. by apply: implyP Pi; apply: a; apply: mem_index_enum. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg poly ssrnum ssrint)