proposition: Lemma gcd1p p : gcdp 1 p %= 1.
proof: Proof. rewrite -size_poly_eq1 gcdpE size_poly1; case: ltnP. by rewrite modp1 gcd0p size_poly1 eqxx. move/size1_polyC=> e; rewrite e. 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)