proposition: Lemma count_root_seq p x : count_mem x (root_seq p) = \mu_x p.
proof: Proof. have [-> | Hp] := eqVneq p 0; first by rewrite root_seq0 mu0. apply/eqP; rewrite -muP //. case/boolP: (x \in root_seq p) => [|H]. rewrite -mem_undup => H. move: (prod_XsubC_count p). rewrite (bigD1_seq x) //= ?undup_uniq //. set b:= \big[_/_]_(_ <- _ | _) _ => Hpq. apply/andP; split; apply/dvdpP. by exists (lead_coef p *: b); rewrite -scalerAl mulrC. case=> q Hq. have H1: ~~ (('X - x%:P) %| b). rewrite dvdp_XsubCl; apply/rootP. rewrite horner_prod; apply/eqP. rewrite (big_nth 0) big_mkord. apply/prodf_neq0=> i Hix. by rewrite horner_exp hornerXsubC expf_neq0 // subr_eq0 eq_sym. have H2: (('X - x%:P) %| b). apply/dvdpP; exists ((lead_coef p)^-1 *: q). apply: (@scalerI _ _ (lead_coef p)); first by rewrite lead_coef_eq0. rewrite -scalerAl scalerA mulrV ?unitfE ?lead_coef_eq0 // scale1r. have HX: (('X - x%:P)^+ (count_mem x (root_seq p))) != 0. by apply: expf_neq0; rewrite -size_poly_eq0 size_XsubC. rewrite -(mulpK (_ *: b) HX) -(mulpK (q * _) HX). by rewrite -scalerAl mulrC -Hpq -mulrA -exprS -Hq. by rewrite H2 in H1. have->: count_mem x (root_seq p) = 0%N by apply/count_memPn. by rewrite dvd1p /= dvdp_XsubCl -root_root_seq. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_real_closed) CoqEAL(ssrcomplements)