proposition: Lemma galois_big_prodv_seq I r (P : {pred I}) (k : {subfield L}) (K : I -> {subfield L}) : (forall i, P i -> galois k (K i)) -> ~~ nilp [seq i <- r | P i] -> galois k (\big[@prodv _ _/1%VS]_(i <- r | P i) K i).
proof: Proof. move=> galkK brP; pose gW := (galois_subW, galois_normalW, galois_separableW). pose bpv := (subv_big_prodv_seq, separable_big_prodvW, normal_big_prodv). by rewrite /galois !bpv// => i Pi; rewrite /= gW ?galkK. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)