Library Coq.micromega.Lia

Require Import ZMicromega.
Require Import ZArith.
Require Import RingMicromega.
Require Import VarMap.
Require Tauto.

Ltac preprocess :=
  zify ; unfold Z.succ in * ; unfold Z.pred in *.

Ltac lia :=
  preprocess;
  xlia ;
  abstract (
      intros __wit __varmap __ff ;
      change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
      apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)).

Ltac nia :=
  preprocess;
  xnlia ;
  abstract (
      intros __wit __varmap __ff ;
      change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
      apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)).