Library Coq.micromega.Lia
Require
Import
ZMicromega
RingMicromega
VarMap
DeclConstant
.
Require
Import
BinNums
.
Require
Coq.micromega.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
;
xnlia
zchecker
.