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
.