proposition: Lemma and_dnfP e bcs1 bcs2 : qf_eval e (dnf_to_form (and_dnf bcs1 bcs2)) = qf_eval e (dnf_to_form bcs1 /\ dnf_to_form bcs2).
proof: Proof. elim: bcs1 => [|bc1 bcs1 IH1] /=; first by rewrite /and_dnf big_nil. rewrite /and_dnf big_cons -/(and_dnf bcs1 bcs2) cat_dnfP /=. rewrite {}IH1 /= andb_orl; congr orb. elim: bcs2 bc1 {bcs1} => [|bc2 bcs2 IH] bc1 /=; first by rewrite andbF. rewrite {}IH /= andb_orr; congr orb => {bcs2}. suffices aux (l1 l2 : seq (term R)) g : let redg := foldr (And \o g) True in qf_eval e (redg (l1 ++ l2)) = qf_eval e (redg l1 /\ redg l2)%T. + by rewrite 2!aux /= 2!andbA -andbA -andbCA andbA andbCA andbA. by elim: l1 => [| t1 l1 IHl1] //=; rewrite -andbA IHl1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)