Library Stdlib.ZArith.ZNsatz

From Stdlib Require Import BinInt Lia NsatzTactic.
Export (ltac.notations) NsatzTactic.

Ltac nsatz_internal_lia ::= lia.

#[export] Existing Instance Zr.

#[export] Instance Zcri : Cring (Rr:=Zr).

#[export] Instance Zdi : Integral_domain (Rcr:=Zcri).