proposition: Lemma mul_polyC_seqmul (R : rcfType) (p : {poly R}) (a : R) : a != 0 -> polyseq (a *: p) = seqmul (nseq (size p) a) p.
proof: Proof. move=> Ha; elim/poly_ind : p => [ | p c IHp]. by rewrite size_poly0 /= seqmul0 -mul_polyC mulr0 -polyC0 polyseq0. rewrite -{2}(cons_poly_def) -mul_polyC mulrDr mulrA mul_polyC -polyCM. rewrite -!cons_poly_def !polyseq_cons. case Hp : (nilp p); last first. rewrite ifT; last first. rewrite nil_poly in Hp. by rewrite nil_poly -mul_polyC mulf_neq0 // ?Hp // polyC_eq0. by rewrite seqmul_cons IHp. rewrite ifF; last first. rewrite nil_poly in Hp. by rewrite nil_poly -mul_polyC mulf_eq0 Hp orbT. rewrite /= size_polyC. have [->|Hc] := eqVneq c 0; first by rewrite mulr0 seqmul0 polyseqC eq_refl. by rewrite !polyseqC mulf_neq0//= Hc seqmul_cons. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol mathcomp(complex)