proposition: Lemma eval_CcountWeak e p sq k k' : (forall x, qf_eval e (k x) = k' (eval e x)) -> qf_eval e (CcountWeak p sq k) = k' (ccount_weak (eval_poly e p) (map (eval_poly e) sq)).
proof: Proof. move=> Pk; rewrite /CcountWeak /ccount_weak. set Aux := (fix Aux s i k := match i with 0 => _ | _ => _ end). set aux := (fix aux s i := match i with 0 => _ | _ => _ end). rewrite size_map -[0]/(eval e 0%qfT); move: 0%qfT=> x. elim: (_ ^ _)%N k k' Pk x=> /= [|n ihn] k k' Pk x. by rewrite Pk. rewrite (eval_TaqsR (fun y => k' (aux (y * (coefs F (size sq) n) + eval e x) n))). by rewrite size_map. by move=> y; rewrite (ihn _ k') // -(eval_Coefs e). 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)