proposition: Lemma qf_to_dnf_rterm f b : rformula f -> all dnf_rterm (qf_to_dnf f b).
proof: Proof. set ok := all dnf_rterm. have cat_ok bcs1 bcs2: ok bcs1 -> ok bcs2 -> ok (bcs1 ++ bcs2). by move=> ok1 ok2; rewrite [ok _]all_cat; apply/andP. have and_ok bcs1 bcs2: ok bcs1 -> ok bcs2 -> ok (and_dnf bcs1 bcs2). rewrite /and_dnf unlock; elim: bcs1 => //= cl1 bcs1 IH1; rewrite -andbA. case/and3P=> ok11 ok12 ok1 ok2; rewrite cat_ok ?{}IH1 {bcs1 ok1}//. elim: bcs2 ok2 => //= cl2 bcs2 IH2 /andP[ok2 /IH2->]. by rewrite /dnf_rterm !all_cat ok11 ok12 /= !andbT. elim: f b => //=; [ by do 2!case | | | | | by auto | | ]; try by repeat case/andP || intro; case: ifP; auto. by rewrite /dnf_rterm => ?? [] /= ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)