Library Stdlib.Reals.RNsatz
From Stdlib Require Import NsatzTactic.
Export (ltac.notations) NsatzTactic.
From Stdlib Require Import Raxioms RIneq DiscrR.
Ltac nsatz_internal_discrR ::= discrR.
#[local] Ltac extra_reify :=
lazymatch goal with |- Ncring_tac.extra_reify _ (IZR ?z) =>
lazymatch isZcst z with
| true => exact (PEc z)
end
end.
#[export] Hint Extern 1 (Ncring_tac.extra_reify _ _) => extra_reify : typeclass_instances.
#[export] Instance Rops: @Ring_ops R 0%R 1%R Rplus Rmult Rminus Ropp (@eq R) := {}.
#[export] Instance Rri : Ring (Ro:=Rops).
#[export] Instance Rcri: (Cring (Rr:=Rri)).
#[export] Instance Rdi : (Integral_domain (Rcr:=Rcri)).