fact: Definition negate {T : Type} (t:Formula Z) (tg:T) : cnf (NFormula Z) T := let f := xnnormalise t in if Zunsat f then cnf_tt _ _ else cnf_of_list tg (xnegate f).
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums