proposition: Lemma terms_of_neq_leq_elim oc1 oc2: oc2 \in (oclause_neq_leq_elim oc1) -> {subset (terms_of_oclause oc2) <= (terms_of_oclause oc1) ++ map Opp oc1.2}.
proof: Proof. rewrite /oclause_neq_leq_elim/flatten; rewrite foldr_map. suff : forall oc3, oc3 \in (oclause_leq_elim oc1) -> (terms_of_oclause oc3 =i terms_of_oclause oc1) /\ oc3.2 = oc1.2. elim: (oclause_leq_elim oc1) => [| t l ih] //= h1. rewrite mem_cat; case/orP. - move/terms_of_neq_elim=> h u; move/(h u); rewrite !mem_cat. by case: (h1 t (mem_head _ _)); move/(_ u)=> -> ->. - by move=> h; apply: (ih _ h) => ? loc3; apply: h1; rewrite in_cons loc3 orbT. move=> {oc2} oc3 hoc3; split; first exact: terms_of_leq_elim. case: oc3 hoc3=> eq2 neq2 lt2 leq2 /=; case: oc1=> eq1 neq1 lt1 leq1 /=. elim: leq1 => [| t1 le1 ih] //=; first by rewrite inE; case/eqP=> _ ->. rewrite map_cat mem_cat; move: ih. elim: (leq_elim_aux eq1 lt1 le1) => [| t2 l2 ih2] //=; rewrite !in_cons. move=> h1; case/orP=> /=. case/orP; first by case/eqP. by move=> h2; apply: ih2; rewrite ?h2 // => - h3; apply: h1; rewrite h3 orbT. case/orP; first by case/eqP. move=> h3; apply: ih2; last by rewrite h3 orbT. by move=> h2; apply: h1; rewrite h2 orbT. 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)