proposition: Lemma size_gcdp1 p : size (gcdp p 1) = 1.
proof: Proof. rewrite gcdpE size_polyC oner_eq0 /= modp1 ltnS; case: leqP. by move/size_poly_leq0P->; rewrite gcdp0 modp0 size_polyC oner_eq0. by rewrite gcd0p size_polyC oner_eq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)