proposition: Lemma dnf_to_rform bcs : rformula (odnf_to_oform bcs) = all dnf_rterm bcs.
proof: Proof. elim: bcs => //= [[cl1 cl2 cl3 cl4] bcs ->]; rewrite {2}/dnf_rterm /=; congr (_ && _). congr andb; first by elim: cl1 => //= t cl ->; rewrite andbT. congr andb; first by elim: cl2 => //= t cl ->; rewrite andbT. congr andb; first by elim: cl3 => //= t cl ->. by elim: cl4 => //= t cl ->. 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)