proposition: Lemma eval_CcountGt0 e sp sq : qf_eval e (CcountGt0 sp sq) = ccount_gt0 (map (eval_poly e) sp) (map (eval_poly e) sq).
proof: Proof. pose sq' := map (eval_poly e) sq; rewrite /ccount_gt0. rewrite (@eval_BigRgcd _ _ _ (fun p => if p != 0 then 0 < ccount_weak p sq' else let bq := bounding_poly sq' in [|| \big[andb/true]_(q <- sq') (0 < lead_coef q), \big[andb/true]_(q <- sq') (0 < (-1) ^+ (size q).-1 * lead_coef q) | 0 < ccount_weak bq sq'])). by rewrite !big_map. move=> p; rewrite eval_Isnull; case: eqP=> _ /=; last first. by rewrite (eval_CcountWeak (> 0)). rewrite (eval_CcountWeak (fun n => [|| \big[andb/true]_(q <- sq') (0 < lead_coef q), \big[andb/true]_(q <- sq') (0 < (-1) ^+ (size q).-1 * lead_coef q) | 0 < n ])). by rewrite eval_BoundingPoly. move=> n /=; rewrite -!bigop.unlock !big_map; congr [|| _, _| _]. apply: (big_ind2 (fun u v => qf_eval e u = v))=> //=. by move=> u v u' v' -> ->. by move=> i _; rewrite (eval_LeadCoef (> 0)). apply: (big_ind2 (fun u v => qf_eval e u = v))=> //=. by move=> u v u' v' -> ->. by move=> i _; rewrite eval_Size (eval_LeadCoef (fun lq => (0 < (-1) ^+ (size (eval_poly e i)).-1 * lq))). Qed.
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)