proposition: Lemma subv_big_prodv_seq I r (P : {pred I}) (k : {subfield L}) (K : I -> {subfield L}) : (forall i, P i -> (k <= K i)%VS) -> ~~ nilp [seq i <- r | P i] -> (k <= \big[@prodv _ _/1]_(i <- r | P i) K i)%VS.
proof: Proof. move=> normkK; elim: r => [|i r IHr]; rewrite !(big_nil, big_cons)//=. case: ifP IHr => //= Pi; rewrite -big_filter. have [->|_ IHr]//= := altP nilP; first by rewrite big_nil prodv1 normkK. by rewrite -[X in (X <= _)%VS]prodv_id prodvS ?IHr ?normkK. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)