proposition: Lemma poly_def_lead_coef : forall p : {poly R}, p = \sum_(i < (size p).-1) p`_i *: 'X^i + lead_coef p *: 'X^(size p).-1.
proof: Proof. move=> p; case sz_p : (size _) => [|n]. - move/eqP: sz_p; rewrite size_poly_eq0; move/eqP => ->. by rewrite big_ord0 /lead_coef coef0 scale0r addr0. - by rewrite -{1}(coefK p) /lead_coef sz_p [_.-1]/= poly_def big_ord_recr /=. Qed.
imports: mathcomp(all_ssreflect fingroup perm ssralg zmodp) mathcomp(matrix mxalgebra poly polydiv mxpoly) ssralg_ext