proposition: Lemma prodv_idPl (F0 : fieldType) (L : fieldExtType F0) (K F : {subfield L}) : reflect (F * K = F)%VS (K <= F)%VS.
proof: Proof. apply: (iffP idP) => [KF|<-]; last by rewrite field_subvMl. by apply/eqP; rewrite eqEsubv prodv_sub//= field_subvMr. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)