proposition: Lemma big_real x0 op I (P : pred I) F (s : seq I) : {in real &, forall x y, op x y \is real} -> x0 \is real -> {in P, forall i, F i \is real} -> \big[op/x0]_(i <- s | P i) F i \is real.
proof: Proof. exact: comparable_bigr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)