proposition: Lemma separable_big_prodv I r (P : {pred I}) (k : {subfield L}) (K : I -> {subfield L}) : separable k (\big[@prodv _ _/1%VS]_(i <- r | P i) K i) = \big[andb/true]_(i <- r | P i) separable k (K i).
proof: Proof. rewrite big_prodv_eq_aspace; elim/big_rec2: _ => [|i E b _]. by rewrite separable1. by rewrite separable_prodv => ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)