proposition: Lemma tail_coefM (p q: {poly R}): tail_coef (p*q) = (tail_coef p) * (tail_coef q).
proof: Proof. rewrite /tail_coef. case pnz: (p!=0); last by rewrite (eqP(negbFE pnz)) mul0r mu0 coef0 mul0r. case qnz: (q!=0); last by rewrite (eqP(negbFE qnz)) mulr0 mu0 coef0 mulr0. rewrite (mu_mul 0 (mulf_neq0 pnz qnz)). move: (mu_spec 0 pnz) (mu_spec 0 qnz); rewrite subr0. set a := (\mu_0 p); set b:= (\mu_0 q); move => [pa v1 ->] [qa v2 ->]. by rewrite mulrACA -exprD 3! coefMXn ! ltnn ! subnn - ! horner_coef0 hornerM. 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)