proposition: Lemma separable_prodv (k K1 K2 : {subfield L}) : separable k (K1 * K2) = (separable k K1 && separable k K2).
proof: Proof. apply/separableP/andP => [sepK12|]. split; apply/separableP => y yK; rewrite sepK12//. by apply: (subv_trans yK); rewrite field_subvMr. by apply: (subv_trans yK); rewrite field_subvMl. move=> [/separableP sepK1 /separableP sepK2]. move=> x /memv_mulP[n [us [vs [/allP/= usK /allP/= vsK ->]]]]. rewrite separable_sum// => i _; rewrite separable_mulv//. by rewrite sepK1 ?usK ?mem_tnth. by rewrite sepK2 ?vsK ?mem_tnth. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)