fact: Fixpoint egcdp_rec p q k {struct k} : {poly R} * {poly R} := if k is k'.+1 then if q == 0 then (1, 0) else let: (u, v) := egcdp_rec q (p %% q) k' in (lead_coef q ^+ scalp p q *: v, (u - v * (p %/ q))) else (1, 0).
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)