proposition: Lemma Bezoutp p q : exists u, u.1 * p + u.2 * q %= (gcdp p q).
proof: Proof. have [-> | pn0] := eqVneq p 0. by rewrite gcd0p; exists (0, 1); rewrite mul0r mul1r add0r. have [-> | qn0] := eqVneq q 0. by rewrite gcdp0; exists (1, 0); rewrite mul0r mul1r addr0. pose e := egcdp p q; exists e; rewrite eqp_sym. by case: (egcdpP pn0 qn0). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)