Library Stdlib.Reals.Nsatz

From Stdlib Require Import List.
From Stdlib Require Import Setoid.
From Stdlib Require Import BinPos.
From Stdlib Require Import BinList.
From Stdlib Require Import Znumtheory.
From Stdlib Require Export Morphisms Setoid Bool.
From Stdlib Require Export Algebra_syntax.
From Stdlib Require Export Ncring.
From Stdlib Require Export Ncring_initial.
From Stdlib Require Export Ncring_tac.
From Stdlib Require Export Integral_domain.
From Stdlib Require Import DiscrR.
From Stdlib Require Import ZArith.
From Stdlib Require Import Lia.

From Stdlib Require Export NsatzTactic.

Ltac nsatz_internal_discrR ::= discrR.

From Stdlib Require Export Rbase.
From Stdlib Require Export Rfunctions.
From Stdlib Require Import RealField.

Lemma Rsth : Setoid_Theory R (@eq R).

#[global]
Instance Rops: (@Ring_ops R 0%R 1%R Rplus Rmult Rminus Ropp (@eq R)).
Defined.

#[global]
Instance Rri : (Ring (Ro:=Rops)).
Defined.

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

Lemma R_one_zero: 1%R <> 0%R.

#[global]
Instance Rcri: (Cring (Rr:=Rri)).


#[global]
Instance Rdi : (Integral_domain (Rcr:=Rcri)).
Defined.