Library Coq.micromega.Lia
Require Import ZMicromega.
Require Import ZArith_base.
Require Import RingMicromega.
Require Import VarMap.
Require Import DeclConstant.
Require Coq.micromega.Tauto.
Ltac zchecker :=
intros __wit __varmap __ff ;
exact (ZTautoChecker_sound __ff __wit
(@eq_refl bool true <: @eq bool (ZTautoChecker __ff __wit) true)
(@find Z Z0 __varmap)).
Ltac lia := PreOmega.zify; xlia zchecker.
Ltac nia := PreOmega.zify; xnlia zchecker.