proposition: Lemma prodv_Fadjoinr (F0 : fieldType) (L : fieldExtType F0) (K F : {subfield L}) (x : L) : (F * <<K; x>>)%VS = <<F * K; x>>%VS.
proof: Proof. by rewrite prodvC prodv_Fadjoinl prodvC. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)