proposition: Lemma mu_spec_supp p: p != 0 -> exists q, [/\ p = q * 'X^ (\mu_0 p), (~~ root q 0), lead_coef p = lead_coef q, tail_coef p = tail_coef q & tail_coef q = q`_0].
proof: Proof. move /(mu_spec 0) => [q pa]; set n := (\mu_0 p) => ->; exists q. rewrite lead_coefM tail_coefM {1 2} subr0 (eqP (monicXn R n)) mulr1 /tail_coef. by rewrite mu_exp mu_XsubC mul1n subr0 coefXn eqxx mulr1 (muNroot pa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polydiv polyorder path interval polyrcf)