proposition: Lemma galois_prodv (k K1 K2 : {subfield L}) : galois k K1 -> galois k K2 -> galois k (K1 * K2).
proof: Proof. rewrite /galois => /and3P[kK1 sepK1 normK1] /and3P[kK2 sepK2 normK2]. rewrite -[X in (X <= _)%VS]prodv_id prodvS//=. by rewrite separable_prodv ?sepK1 ?sepK2// normal_prodv. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)