proposition: Lemma tail_coefE p: tail_coef p = (head 0 (filter0 p)).
proof: Proof. have [-> |] := (eqVneq p 0); first by rewrite /tail_coef mu0 coef0 polyseq0 /=. move /(mu_spec_supp) => [q [pa pb pc pd pe]]; rewrite /filter0. case (eqVneq q 0) => qnz; first by move: pb; rewrite qnz root0. have q0nz: q`_0 != 0 by rewrite - horner_coef0. rewrite pd pe pa polyseqMXn// -cat_nseq filter_cat (eq_in_filter (a2 := pred0)). by rewrite filter_pred0 cat0s nth0; move: q0nz; case q; case => //= a l _ ->. have /allP h: all (pred1 (0:R)) (nseq (\mu_0 p) 0). by rewrite all_pred1_nseq. by move => x /h /= ->. 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)