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
.