fact: Definition odnf_to_oform := let pos_lit t := And (t == 0)%oT in let neg_lit t := And (t != 0)%oT in let lt_lit t := And (0 <% t)%oT in let le_lit t := And (0 <=% t)%oT in let ocls (bc : oclause R) := Or (foldr pos_lit True bc.1 /\ foldr neg_lit True bc.2 /\ foldr lt_lit True bc.3 /\ foldr le_lit True bc.4) in foldr ocls False.
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)