fact: Definition xnegate (f:NFormula Z) : list (NFormula Z) := let (e,o) := f in match o with | Equal => (e,Equal) :: nil | NonEqual => (psub e (Pc 1),NonStrict) :: (psub (Pc (-1)) e, NonStrict) :: nil | NonStrict => (e,NonStrict)::nil | Strict => (psub e (Pc 1),NonStrict)::nil end.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums