proposition: Lemma gdcop_eq0 p q : (gdcop p q == 0) = (q == 0) && (p != 0).
proof: Proof. have [->|q0] := eqVneq q. by rewrite gdcop0 /=; case: (p == 0); rewrite ?eqxx ?oner_eq0. rewrite /gdcop; move: {-1}(size q) (leqnn (size q))=> k hk; apply: negPf. elim: k q q0 hk => [|k ihk] /= q q0 hk. by move: hk q0; rewrite leqn0 size_poly_eq0; move->. case: ifP=> cpq; first by rewrite (negPf q0). apply: ihk. rewrite divpN0; last by rewrite gcdp_eq0 negb_and q0. by rewrite dvdp_leq // dvdp_gcdl. rewrite -ltnS; apply: leq_trans hk; move: (dvdp_gcdl q p); rewrite dvdp_eq. move/eqP=> eqq; move/(f_equal (fun x : {poly R} => size x)): (eqq). rewrite size_scale; last exact: lc_expn_scalp_neq0. have gcdn0 : gcdp q p != 0 by rewrite gcdp_eq0 negb_and q0. have qqn0 : q %/ gcdp q p != 0. apply: contraNneq q0 => e. move: (scaler_eq0 (lead_coef (gcdp q p) ^+ scalp q (gcdp q p)) q). by rewrite (negPf (lc_expn_scalp_neq0 _ _)) /= eqq e mul0r eqxx. move->; rewrite size_mul //; case sgcd: (size (gcdp q p)) => [|n]. by move/eqP: sgcd gcdn0; rewrite size_poly_eq0; move->. case: n sgcd => [|n]; first by move/eqP; rewrite size_poly_eq1 gcdp_eqp1 cpq. by rewrite addnS /= -{1}[size (_ %/ _)]addn0 ltn_add2l. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg poly polydiv ssrnum zmodp) mathcomp(polyorder path interval ssrint)