proposition: Lemma mupMl x q1 q2 : ~~ root q1 x -> mup x (q1 * q2) = mup x q2.
proof: Proof. move=> q1Nx; have q1N0 : q1 != 0 by apply: contraNneq q1Nx => ->; rewrite root0. have [->|q2N0] := eqVneq q2 0; first by rewrite mulr0. apply/esym/eqP; rewrite eqn_leq mup_geq ?mulf_neq0// dvdp_mull -?mup_geq//=. rewrite mup_leq ?mulf_neq0// Gauss_dvdpr -?mup_ltn//. by rewrite coprimep_expl// coprimep_sym coprimep_XsubC. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)