fact: Fixpoint rgcdp_loop n (pp qq : {poly F}) {struct n} := let rr := rmodp pp qq in if rr == 0 then qq else if n is n1.+1 then rgcdp_loop n1 qq rr else rr.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice ssrnat seq) mathcomp(fintype generic_quotient bigop ssralg poly) mathcomp(polydiv matrix mxpoly countalg ring_quotient)