proposition: Lemma egcdpE p q (e := egcdp p q) : gcdp p q %= e.1 * p + e.2 * q.
proof: Proof. rewrite {}/e; have [-> /= | qn0] := eqVneq q 0. by rewrite gcdp0 egcdp0 mul1r mulr0 addr0. have [-> | pn0] := eqVneq p 0; last by case: (egcdpP pn0 qn0). by rewrite gcd0p /egcdp size_poly0 size_poly_leq0 (negPf qn0) /= !simp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)