proposition: Lemma qf_to_dnf_rterm f b : rformula f -> all dnf_rterm (qf_to_odnf 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_odnf bcs1 bcs2). rewrite /and_odnf 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 andbT ok11; case/and3P: ok12=> -> -> ->. elim: f b => //=; [ by move=> [] [] | by move=> ? ? []; rewrite /dnf_rterm /= !andbT | by move=> ? ? []; rewrite /dnf_rterm /= !andbT andbC | by move=> ? ? [] /andP[]; rewrite /dnf_rterm/= => -> -> | by move=> f hf g hg [] /andP[/hf ? /hg ?]; auto | by move=> f hf g hg [] /andP[/hf ? /hg ?]; auto | by move=> f hf g hg [] /andP[/hf ? /hg ?]; auto | by move=> ? h [] /= /h | by move=> _ ? ? [] | by move=> _ ? ? [] ]. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq div choice fintype) mathcomp(bigop order ssralg finset fingroup zmodp) mathcomp(poly ssrnum)