Library Coq.micromega.Lia

Require Import ZMicromega RingMicromega VarMap DeclConstant.
Require Import BinNums.
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 := Zify.zify; xlia zchecker.

Ltac nia := Zify.zify; xnlia zchecker.