proposition: Lemma dnf_rterm_subproof bc : dnf_rterm bc -> all (dnf_rterm \o w_to_oclause) (oclause_to_w bc).
proof: Proof. case: bc => leq lneql llt lle; rewrite /dnf_rterm /=; case/and4P=> req rneq rlt rle. rewrite /oclause_to_w /= !all_map. apply/allP => [] [oc_eq oc_neq oc_le oc_lt] hoc; rewrite /dnf_rterm /= andbT. rewrite -all_cat; apply/allP=> u hu; move/terms_of_neq_leq_elim: hoc => /=. move/(_ u); rewrite !mem_cat. have {}hu : [|| u \in oc_eq, u \in oc_neq, u \in oc_le | u \in oc_lt]. by move: hu; rewrite mem_cat; case/orP=> ->; rewrite ?orbT. move/(_ hu); case/orP; last first. move: rneq. have <- : (all (@rterm R) (map Opp lneql)) = all (@rterm R) lneql. by elim: lneql => [| t l] //= ->. by move/allP; apply. case/orP; first by apply: (allP req). case/orP; first by apply: (allP rneq). case/orP; first by apply: (allP rlt). exact: (allP rle). 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)