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)).