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.

Ltac Ncring_tac.extra_reify term ::=
  lazymatch term with
  | IZR ?z =>
      lazymatch isZcst z with
      | true => open_constr:(PEc z)
      | false => open_constr:(tt)
      end
  | _ => open_constr:(tt)
  end.

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