fact: Fixpoint rgdcop_recT n (q : polyF) (p : polyF) := if n is m.+1 then 'let g <- rgcdpT p q; 'let sg <- sizeT g; if sg == 1 then ret p else 'let r <- rdivpT p g; rgdcop_recT m q r else 'let b <- isnull q; ret [::b%:R%T].
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)