proposition: Lemma mupM x q1 q2 : q1 != 0 -> q2 != 0 -> mup x (q1 * q2) = (mup x q1 + mup x q2)%N.
proof: Proof. move=> q1N0 q2N0; apply/eqP; rewrite eqn_leq mup_leq ?mulf_neq0//. rewrite mup_geq ?mulf_neq0// exprD ?dvdp_mul; do ?by rewrite -mup_geq. have [m1 [r1]] := multiplicity_XsubC q1 x; rewrite q1N0 /= => r1Nx ->. have [m2 [r2]] := multiplicity_XsubC q2 x; rewrite q2N0 /= => r2Nx ->. rewrite !mupMl// ?mup_XsubCX eqxx/= mulrACA exprS exprD. rewrite dvdp_mul2r ?mulf_neq0 ?expf_neq0 ?polyXsubC_eq0//. by rewrite dvdp_XsubCl rootM negb_or r1Nx r2Nx. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)