fact: Definition Zeval_bop2 (o : Op2) : Z -> Z -> bool := match o with | OpEq => Z.eqb | OpNEq => fun x y => negb (Z.eqb x y) | OpLe => Z.leb | OpGe => Z.geb | OpLt => Z.ltb | OpGt => Z.gtb end.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing