proposition: Lemma ccount_weakP p sq : p != 0 -> reflect (exists x, (p.[x] == 0) && \big[andb/true]_(q <- sq) (q.[x] > 0)) (ccount_weak p sq > 0).
proof: Proof. move=> p_neq0; rewrite -constraints1P /constraints ltr0n lt0n. rewrite -(@pnatr_eq0 [numDomainType of int]) natr_sum psumr_eq0 //. rewrite -has_predC /=. apply: (iffP hasP) => [[x rpx /= prod_neq0]|[x /andP[rpx]]]. exists x; rewrite -rootE [root _ _]roots_on_rootsR // rpx /=. rewrite big_seq big1 => // q Hq. move: prod_neq0; rewrite pnatr_eq0 -lt0n => /all_prodn_gt0. have := index_mem q sq; rewrite Hq => Hoq. pose oq := Ordinal Hoq => /(_ oq). rewrite mem_index_enum => /(_ isT isT) /=. by rewrite nth_nseq index_mem Hq nth_index // lt0b sgz_cp0. rewrite big_all => /allP Hsq. exists x => /=; first by rewrite -roots_on_rootsR. rewrite pnatr_eq0 -lt0n prodn_gt0 => // i; rewrite nth_nseq ltn_ord lt0b. by rewrite sgz_cp0 Hsq // mem_nth. Qed.
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)