proposition: Lemma size_gcd1p p : size (gcdp 1 p) = 1.
proof: Proof. rewrite gcdpE size_polyC oner_eq0 /= modp1; have [|/size1_polyC ->] := ltnP. by rewrite gcd0p size_polyC oner_eq0. have [->|p00] := eqVneq p`_0 0; first by rewrite modp0 gcdp0 size_poly1. by rewrite modpC // gcd0p size_polyC p00. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)