proposition: Lemma subv_big_prodv (I : finType) (D : {pred I}) (k : {subfield L}) (K : I -> {subfield L}) : (#|D| > 0)%N -> (forall i, D i -> k <= K i)%VS -> (k <= \big[@prodv _ _/1]_(i in D) K i)%VS.
proof: Proof. move=> D_gt0 DK; apply: subv_big_prodv_seq => //. by rewrite /nilp size_filter -sum1_count sum1_card -lt0n. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)