fact: Definition xnnormalise (t : Formula Z) : NFormula Z := let (lhs,o,rhs) := t in let lhs := normZ lhs in let rhs := normZ rhs in match o with | OpEq => (psub rhs lhs, Equal) | OpNEq => (psub rhs lhs, NonEqual) | OpGt => (psub lhs rhs, Strict) | OpLt => (psub rhs lhs, Strict) | OpGe => (psub lhs rhs, NonStrict) | OpLe => (psub rhs lhs, NonStrict) end.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing