proposition: Lemma mupNroot (x : L) q : ~~ root q x -> mup x q = 0%N.
proof: Proof. move=> qNx; have qN0 : q != 0 by apply: contraNneq qNx => ->; rewrite root0. by move: qNx; rewrite -dvdp_XsubCl XsubC_dvd// lt0n negbK => /eqP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)