proposition: Lemma polyseq_deg2 (a b c : R) : a != 0 -> (a *: 'X^2 + b *: 'X + c%:P) = [:: c; b; a] :> seq R.
proof: Proof. move=> Ha. rewrite -(mul_polyC a) -(mul_polyC b) expr2 mulrA -mulrDl. by rewrite -cons_poly_def polyseq_cons mul_polyC polyseq_deg1. 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)