Library Stdlib.QArith.QNsatz

From Stdlib.nsatz Require Import NsatzTactic.
Export (ltac.notations) NsatzTactic.

From Stdlib.QArith Require Import QArith_base.

#[export] Instance Qops: @Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq := {}.

#[export]
Instance Qri : Ring (Ro:=Qops).

#[export] Instance Qcri: Cring (Rr:=Qri).

#[export] Instance Qdi : Integral_domain (Rcr:=Qcri).