proposition: Lemma prodr_ge0 I r (P : pred I) (E : I -> R) : (forall i, P i -> 0 <= E i) -> 0 <= \prod_(i <- r | P i) E i.
proof: Proof. by move=> Ege0; rewrite -nnegrE rpred_prod. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)