proposition: Lemma separable_big_prodvW I r (P : {pred I}) (k : {subfield L}) (K : I -> {subfield L}) : (forall i, P i -> separable k (K i)) -> separable k (\big[@prodv _ _/1%VS]_(i <- r | P i) K i).
proof: Proof. move=> sepKi; rewrite separable_big_prodv big_tnth big_andE. by apply/'forall_implyP => i /sepKi. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)