proposition: Lemma prod_real I (P : pred I) (F : I -> R) (s : seq I) : {in P, forall i, F i \is real} -> \prod_(i <- s | P i) F i \is real.
proof: Proof. by apply/big_real; [apply: rpredM | apply: rpred1]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)