proposition: Lemma prodv_sub_normalClosure E F : (E * F <= normalClosure E F)%VS.
proof: Proof. rewrite /normalClosure (bigD1 \1%AF) ?group1//= lim1g. by rewrite big_prodv_eq_aspace field_subvMr. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)