proposition: Lemma valid_QE_wproj i bc (bc' := w_to_oclause bc) (ex_i_bc := ('exists 'X_i, odnf_to_oform [:: bc'])%oT) e : dnf_rterm bc' -> reflect (holds e ex_i_bc) (ord.qf_eval e (wproj i bc)).
proof: Proof. case: bc @bc' @ex_i_bc=> sp sq /=; rewrite /dnf_rterm /wproj /= andbT. move=> /andP[rsp rsq]; rewrite -qf_evalE. rewrite eval_CcountGt0 /=; apply: (equivP (ccount_gt0P _ _)). set P1 := (fun x => _); set P2 := (fun x => _). suff: forall x, P1 x <-> P2 x. by move=> hP; split=> [] [x Px]; exists x; rewrite (hP, =^~ hP). move=> x; rewrite /P1 /P2 {P1 P2} !big_map !(big_seq_cond xpredT) /=. rewrite (eq_bigr (fun t => GRing.eval (set_nth 0 e i x) t == 0)); last first. by move=> t /andP[t_in_sp _]; rewrite abstrXP evalE to_rtermE ?(allP rsp). rewrite [X in _ && X](eq_bigr (fun t => 0 < GRing.eval (set_nth 0 e i x) t)); last by move=> t /andP[tsq _]; rewrite abstrXP evalE to_rtermE ?(allP rsq). rewrite -!big_seq_cond !(rwP (qf_evalP _ _)); first last. + elim: sp rsp => //= p sp ihsp /andP[rp rsp]; first by rewrite ihsp. + elim: sq rsq => //= q sq ihsq /andP[rq rsq]; first by rewrite ihsq. rewrite !(rwP andP) (rwP orP) orbF !andbT /=. have unfoldr P s : foldr (fun t => ord.And (P t)) ord.True s = \big[ord.And/ord.True]_(t <- s) P t by rewrite unlock /reducebig. rewrite !unfoldr; set e' := set_nth _ _ _ _. by rewrite !(@big_morph _ _ (ord.qf_eval _) true andb). 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)