proposition: Lemma oclause_leq_elimP oc e : holds e (odnf_to_oform [:: oc]) <-> holds e (odnf_to_oform (oclause_leq_elim oc)).
proof: Proof. case: oc => eq_l neq_l lt_l le_l; rewrite /oclause_leq_elim. elim: le_l eq_l neq_l lt_l => [|t le_l ih] eq_l neq_l lt_l //=. move: (ih eq_l neq_l lt_l) => /= {ih}. set x1 := foldr _ _ _; set x2 := foldr _ _ _; set x3 := foldr _ _ _. set x4 := foldr _ _ _ => h. have -> : (holds e x1 /\ holds e x2 /\ holds e x3 /\ 0%:R <= eval e t /\ holds e x4 \/ false) <-> (0%:R <= eval e t) /\ (holds e x1 /\ holds e x2 /\ holds e x3 /\ holds e x4 \/ false). split; first by case=> //; do 4!(case=> ?); move=> ?; split => //; left. by case=> ?; case=> //; do 3!(case=> ?); move=> ?; left. rewrite h {h} /= !map_cat /= -!map_comp. set s1 := [seq _ | _ <- _]; set s2 := [seq _ | _ <- _]. set s3 := [seq _ | _ <- _]. rewrite odnf_to_oform_cat. suff {x1 x2 x3 x4} /= -> : holds e (odnf_to_oform s2) <-> eval e t == 0%:R /\ holds e (odnf_to_oform s1). suff /= -> : holds e (odnf_to_oform s3) <-> 0%:R < eval e t /\ holds e (odnf_to_oform s1). rewrite le_eqVlt eq_sym; split; first by case; case/orP=> -> ?; [left|right]. by case; [case=> -> ? /= |case=> ->; rewrite orbT]. rewrite /s1 /s3. elim: (leq_elim_aux eq_l lt_l le_l) => /= [| t1 l ih]; first by split=> // [[]]. rewrite /= ih; split. case; last by case=> -> ?; split=> //; right. by do 2!case=> ?; case; case=> -> ? _; split => //; auto. by case=> ->; case; [do 3!case=> ?; move=> _; left | right]. rewrite /s2 /s1. elim: (leq_elim_aux eq_l lt_l le_l) => /= [| t1 l ih]; first by split=> // [[]]. rewrite /= ih; split. case; last by case=> -> ?; split=> //; right. by case; case=> /eqP ? ?; do 2!case=> ?; move=> _; split=> //; left. case=> /eqP ?; case; first by do 3!case=> ?; move=> _; left. by right; split=> //; apply/eqP. 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)