proposition: Lemma egcdpP p q : p != 0 -> q != 0 -> forall (e := egcdp p q), [/\ size e.1 <= size q, size e.2 <= size p & gcdp p q %= e.1 * p + e.2 * q].
proof: Proof. rewrite /egcdp => pn0 qn0; case: (leqP (size q) (size p)) => /= [|/ltnW] hp. exact: egcdp_recP. case: (egcdp_recP pn0 (leqnn (size p)) hp) => h1 h2 h3; split => //. by rewrite (eqp_ltrans (gcdpC _ _)) addrC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)