fact: Definition Rediv (p : polyF) (q : polyF) : cps (nat * polyF * polyF) := fun k => bind b <- Isnull q; if b then k (0%N, [::Const 0], p) else bind sq <- Size q; bind sp <- Size p; bind lq <- LeadCoef q; Rediv_rec_loop q sq lq 0 [::Const 0] p sp k.
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)