proposition: Lemma oclause_neq_leq_elimP oc e : holds e (odnf_to_oform [:: oc]) <-> holds e (odnf_to_oform (oclause_neq_leq_elim oc)).
proof: Proof. rewrite /oclause_neq_leq_elim. rewrite oclause_leq_elimP; elim: (oclause_leq_elim oc) => [| t l ih] //=. rewrite odnf_to_oform_cat /= ih -oclause_neq_elimP /=. suff -> : forall A, A \/ false <-> A by []. by intuition. 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)