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