fact: Definition ccount_gt0 (sp sq : seq {poly R}) := let p := \big[@rgcdp _/0%R]_(p <- sp) p in if p != 0 then 0 < ccount_weak p sq else let bq := bounding_poly sq in [|| \big[andb/true]_(q <- sq)(lead_coef q > 0) , \big[andb/true]_(q <- sq)((-1)^+(size q).-1 *(lead_coef q) > 0) | 0 < ccount_weak bq sq].
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice path fintype) mathcomp(div bigop order ssralg poly polydiv ssrnum perm zmodp ssrint) mathcomp(polyorder polyrcf interval matrix mxtens)