proposition: Lemma wf_QE_wproj i bc (bc_i := @wproj F i bc) : dnf_rterm (w_to_oclause bc) -> qf_form bc_i && rformula bc_i.
proof: Proof. case: bc @bc_i=> sp sq /=; rewrite /dnf_rterm /= /wproj andbT=> /andP[rsp rsq]. by rewrite qf_formF rformulaF. 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)