proposition: Lemma separable_mul p q : separable (p * q) = [&& separable p, separable q & coprimep p q].
proof: Proof. apply/idP/and3P => [sep_pq | [sep_p sep_q co_pq]]. rewrite !(dvdp_separable _ sep_pq) ?dvdp_mulIr ?dvdp_mulIl //. by rewrite (separable_coprime sep_pq). rewrite unlock in sep_p sep_q *. rewrite derivM coprimepMl {1}addrC mulrC !coprimep_addl_mul. by rewrite !coprimepMr (coprimep_sym q p) co_pq !andbT; apply/andP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop finset prime) mathcomp(binomial ssralg poly polydiv fingroup perm) mathcomp(morphism quotient gproduct finalg zmodp cyclic) mathcomp(matrix mxalgebra mxpoly polyXY vector falgebra) mathcomp(fieldext)