proposition: Lemma size_pp : forall p, size p = size (pp p).
proof: Proof. move=> p. have [-> | p0] := eqVneq p 0; first by rewrite pp0. have gp0: (gcdsr p != 0) by rewrite gcdsr_eq0. apply/eqP; rewrite eqn_leq; apply/andP; split. move: (size_mul_leq (gcdsr p)%:P (pp p)). by rewrite {5}(ppP p) size_polyC gp0. rewrite {2}(ppP p). elim/poly_ind: (pp p)=> [|q c IH]; first by rewrite size_poly0 leq0n. rewrite mulrDr mulrA -polyCM !size_MXaddC. case: ifP=>[|H]; first by rewrite leq0n. case: ifP=>//. case/andP=> H1 H2. rewrite mulf_eq0 in H2. case/orP: H2 => G; first by rewrite G in gp0. case/nandP: H=> H; last by move: H; rewrite G. move: H1; rewrite mulf_eq0 -[q == 0]size_poly_eq0. case/orP; rewrite ?polyC_eq0=> H2; first by move: gp0; rewrite H2. move: H2; rewrite size_poly_eq0 => H2. by move: H; rewrite H2. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(path choice fintype tuple finset ssralg) mathcomp(matrix poly) mathcomp(bigop polydiv) CoqEAL(stronglydiscrete dvdring)