proposition: Lemma prodR_ge0 (A : finType) F : (forall a, 0 <= F a) -> 0 <= \prod_(a : A) F a.
proof: Proof. by move=> F0; elim/big_ind : _ => // x y ? ?; exact: mulR_ge0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)