fact: Definition Zeval_op1 (o : Op1) : Z -> Prop := match o with | Equal => fun x : Z => x = 0 | NonEqual => fun x : Z => x <> 0 | Strict => fun x : Z => 0 < x | NonStrict => fun x : Z => 0 <= x end.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing