fact: Definition CcountGt0 (sp sq : seq polyF) : fF := bind p <- BigRgcd sp; bind p0 <- Isnull p; if ~~ p0 then bind c <- CcountWeak p sq; Lt 0%qfT c else let bq := BoundingPoly sq in bind cw <- CcountWeak bq sq; ((reducebig True sq (fun q => BigBody q And true (LeadCoef q (fun lq => Lt 0 lq)))) \/ ((reducebig True sq (fun q => BigBody q And true (bind sq <- Size q; bind lq <- LeadCoef q; Lt 0 ((Opp 1) ^+ (sq).-1 * lq) ))) \/ Lt 0 cw))%qfT.
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)