Library Stdlib.micromega.Lia

From Stdlib Require Import PreOmega ZMicromega RingMicromega VarMap DeclConstantZ.
From Stdlib Require Import BinNums.
From Stdlib.micromega Require Tauto.

Ltac zchecker :=
  let __wit := fresh "__wit" in
  let __varmap := fresh "__varmap" in
  let __ff := fresh "__ff" in
  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; xnia zchecker.