proposition: Lemma size_sub (p q : {poly R}) : p <> 0 -> size p = size q -> lead_coef p = lead_coef q -> size (p - q) < size p.
proof: Proof. move=> p0 pq lc_pq. move: (size_add p (-q)); rewrite pq size_opp (maxn_idPr _) //. rewrite leq_eqVlt; case/orP => // abs. rewrite (@leq_ltn_trans (size q).-1) //; last first. by rewrite -pq prednK // lt0n size_poly_eq0; apply/eqP. rewrite (poly_def_lead_coef p) {1}(poly_def_lead_coef q) lc_pq pq. rewrite opprD addrCA addrK addrC. rewrite (_ : _ - _ = \poly_(i < (size q).-1) (p`_i - q`_i)) ?size_poly //. rewrite -sumrB poly_def; apply eq_bigr => i _; by rewrite scalerBl. Qed.
imports: mathcomp(all_ssreflect fingroup perm ssralg zmodp) mathcomp(matrix mxalgebra poly polydiv mxpoly) ssralg_ext