fact: Definition Zeval_pop2 (o : Op2) : Z -> Z -> Prop := match o with | OpEq => @eq Z | OpNEq => fun x y => ~ x = y | OpLe => Z.le | OpGe => Z.ge | OpLt => Z.lt | OpGt => Z.gt end.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing