proposition: Lemma size_lead_coefK : forall n (p : {poly R}), size p <= n.+1 -> size (p - lead_coef p *: 'X^(size p).-1) <= n.
proof: Proof. elim=> [|n IHn] p sz_p. - rewrite (size1_polyC sz_p) lead_coefC size_polyC. set t := (_ != _); have -> : t.-1 = O by case: t. by rewrite expr0 alg_polyC subrr size_poly0. - rewrite {1}(poly_def_lead_coef p) -addrA subrr addr0; eapply leq_trans. + by rewrite -poly_def; apply size_poly. + by move: sz_p; case: (size _). Qed.
imports: mathcomp(all_ssreflect fingroup perm ssralg zmodp) mathcomp(matrix mxalgebra poly polydiv mxpoly) ssralg_ext