proposition: Lemma prod_truncK I r (P : pred I) F : (forall i, P i -> F i \is a nat_num) -> (\prod_(i <- r | P i) trunc (F i))%:R = \prod_(i <- r | P i) F i.
proof: Proof. by move=> natr; rewrite natr_prod; apply: eq_bigr => i Pi; rewrite truncK ?natr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg poly ssrnum ssrint)