proposition: Lemma oclause_neq_elimP oc e : holds e (odnf_to_oform [:: oc]) <-> holds e (odnf_to_oform (oclause_neq_elim oc)).
proof: Proof. case: oc => eq_l neq_l lt_l le_l; rewrite /oclause_neq_elim. elim: neq_l lt_l => [|t neq_l ih] lt_l //=. move: (ih lt_l) => /= {ih}. set x1 := foldr _ _ _; set x2 := foldr _ _ _; set x3 := foldr _ _ _. set x4 := foldr _ _ _ => h /=. have -> : holds e x1 /\ (eval e t <> 0%:R /\ holds e x2) /\ holds e x3 /\ holds e x4 \/ false <-> (eval e t <> 0%:R) /\ (holds e x1 /\ holds e x2 /\ holds e x3 /\ holds e x4 \/ false). split; case=> //. - by case=> ?; case; case=> ? ? [] ? ?; split=> //; left. - by move=> ?; 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) <-> 0%:R < eval e t/\ 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 oppr_gt0; split. by case; move/eqP; rewrite neq_lt; case/orP=> -> h1; [right | left]. by case; case=> h ?; split=> //; apply/eqP; rewrite neq_lt h ?orbT. rewrite /s1 /s3. elim: (neq_elim_aux lt_l neq_l) => /= [| t1 l ih] /=; first by split => //; case. set y1 := foldr _ _ _; set y2 := foldr _ _ _; set y3 := foldr _ _ _. rewrite ih; split. case; first by case=> ?; case=> _; case; case=> -> ? ?; split=> //; left. by case=> ? ?; split=> //; right. by case=> ->; case; [case=> ?; case=> _; case=> ? ?; left| move=> ?; right]. rewrite /s1 /s2. elim: (neq_elim_aux lt_l neq_l) => /= [| t1 l ih] /=; first by split => //; case. set y1 := foldr _ _ _; set y2 := foldr _ _ _; set y3 := foldr _ _ _. rewrite ih; split. case; first by case=> ? [] _ [] [] ? ? ?; split=> //; left. by case=> ? ?; split=> //; right. case=> ? []; last by right. by case=> ? [] _ [] ? ?; left. 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)