proposition: Lemma gdcop_eq0 (p q : {poly F}) : (gdcop p q == 0)%B = (q == 0)%B && (p != 0)%B.
proof: Proof. have [[->|q_neq0] [->|p_neq0] /=] := (altP (q =P 0), altP (p =P 0)). + by rewrite gdcop0 eqxx oner_eq0. + by rewrite gdcop0 (negPf p_neq0) eqxx. + apply/negP=> /eqP hg; have := coprimep_gdco 0 q_neq0. by rewrite hg coprimep0 eqp01. by apply/negP=> /eqP hg; have := dvdp_gdco p q; rewrite hg dvd0p; apply/negP. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial bigenough)