proposition: Lemma ccount_gt0P (sp sq : seq {poly R}) : reflect (exists x, \big[andb/true]_(p <- sp) (p.[x] == 0) && \big[andb/true]_(q <- sq) (q.[x] > 0)) (ccount_gt0 sp sq).
proof: Proof. rewrite /ccount_gt0; case: (boolP (_ == 0))=> hsp /=; last first. apply: (iffP (ccount_weakP _ _)) => // [] [x Hx]; exists x; by move: Hx; rewrite -rootE root_bigrgcd -big_all. apply: (@equivP (exists x, \big[andb/true]_(q <- sq) (0 < q.[x]))); last first. split=> [] [x Hx]; exists x; rewrite ?Hx ?andbT; do ?by case/andP: Hx. move: hsp; rewrite (big_morph _ (@rgcdp_eq0 _) (eqxx _)) !big_all. by move=> /allP Hsp; apply/allP => p /Hsp /eqP ->; rewrite horner0. have [|bq_neq0] := boolP (bounding_poly sq == 0). rewrite /bounding_poly -derivn1 -derivn_poly0 => ssq_le1. rewrite -constraints1P (size1_polyC ssq_le1) derivnC /= rootsRC. rewrite /constraints big_nil ltxx orbF. move: ssq_le1; rewrite leq_eqVlt ltnS leqn0 orbC. have [|_ /=] := boolP (_ == _). rewrite size_poly_eq0 => /eqP sq_eq0; move/eqP: (sq_eq0). rewrite prodf_seq_eq0 => /hasP /sig2W [q /= q_sq] /eqP q_eq0. move: q_sq; rewrite q_eq0 => sq0 _ {q q_eq0}. set f := _ || _; suff -> : f = false; move: @f => /=. constructor => [] [x]; rewrite big_all. by move=> /allP /(_ _ sq0); rewrite horner0 ltxx. apply: negbTE; rewrite !negb_or !big_all -!has_predC. apply/andP; split; apply/hasP; by exists 0; rewrite //= ?lead_coef0 ?mulr0 ltxx. move=> /size_prod_eq1 Hsq. have {}Hsq q : q \in sq -> q = (lead_coef q)%:P. by move=> /Hsq sq1; rewrite [q]size1_polyC ?sq1 // lead_coefC. apply: (@equivP (\big[andb/true]_(q <- sq) (0 < lead_coef q))); last first. split; [move=> sq0; exists 0; move: sq0|move=> [x]]; rewrite !big_all => /allP H; apply/allP => q q_sq; have:= H _ q_sq; by rewrite [q]Hsq ?lead_coefC ?hornerC. have [] := boolP (\big[andb/true]_(q <- _) (0 < lead_coef q)). by constructor. rewrite !big_all -has_predC => /hasP sq0; apply: (iffP allP) => //=. move: sq0 => [q q_sq /= lq_gt0 /(_ _ q_sq)]. rewrite [q]Hsq ?size_polyC ?lead_coefC //. by case: (_ != 0); rewrite /= expr0 mul1r ?(negPf lq_gt0). apply: (iffP or3P); rewrite -bounding_polyP; case; do ?by [constructor 1|constructor 2]; by move/(ccount_weakP _ bq_neq0); constructor 3. 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)