proposition: Lemma mup_XsubCX n (x y : L) : mup x (('X - y%:P) ^+ n) = (if (y == x) then n else 0)%N.
proof: Proof. have Xxn0 : ('X - y%:P) ^+ n != 0 by rewrite ?expf_neq0 ?polyXsubC_eq0. apply/eqP; rewrite eqn_leq mup_leq ?mup_geq//. have [->|Nxy] := eqVneq x y. by rewrite /= dvdpp ?dvdp_Pexp2l ?size_XsubC ?ltnn. by rewrite dvd1p dvdp_XsubCl /root !hornerE ?horner_exp ?hornerE expf_neq0// subr_eq0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)