proposition: Lemma seqn0_nseq : forall (s : seq R) (a : R), a != 0 -> seqmul (nseq (size (seqn0 s)) a) (seqn0 s) = seqn0 (seqmul (nseq (size s) a) s).
proof: Proof. elim => [ | c l IHl a Ha] //. case Hc : (c != 0). have Hac : a * c != 0 by apply: mulf_neq0. by rewrite seqmul_cons /= Hac /= Hc /= seqmul_cons /= -IHl. have Hac : (a * c != 0) = false by rewrite mulf_eq0 negb_or Ha Hc. by rewrite seqmul_cons /= Hc /= Hac /= IHl. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol mathcomp(complex)