proposition: Lemma polyseq_deg1 (a b : R) : a != 0 -> (a *: 'X + b%:P) = [::b; a] :> seq R.
proof: Proof. move=> H. by rewrite -mul_polyC -cons_poly_def polyseq_cons nil_poly polyC_eq0 polyseqC H. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path choice fintype order) mathcomp(prime div bigop ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex)