proposition: Lemma leq_gcdpl p q : p != 0 -> size (gcdp p q) <= size p.
proof: Proof. by move=> pn0; move: (dvdp_gcdl p q); apply: dvdp_leq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)