proposition: Lemma mup_geq x q n : q != 0 -> (n <= mup x q)%N = (('X - x%:P) ^+ n %| q).
proof: Proof. move=> q_neq0; rewrite /mup; symmetry. case: arg_maxnP; rewrite ?expr0 ?dvd1p//= => i i_dvd gti. case: ltnP => [|/dvdp_exp2l/dvdp_trans]; last exact. apply: contraTF => dvdq; rewrite -leqNgt. suff n_small : (n < (size q).+1)%N by exact: (gti (Ordinal n_small)). by rewrite ltnS ltnW// -(size_exp_XsubC _ x) dvdp_leq. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)