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