fact: Fixpoint rgcdp_loop n (pp qq : {poly F}) {struct n} := if rmodp pp qq == 0 then qq else if n is n1.+1 then rgcdp_loop n1 qq (rmodp pp qq) else rmodp pp qq.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(finfun path matrix) mathcomp(bigop order ssralg poly polydiv ssrnum zmodp div ssrint) mathcomp(polyorder polyrcf interval polyXY) mathcomp(qe_rcf_th ordered_qelim mxtens)