Library Coq.nsatz.Nsatz

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

Require Export NsatzTactic.

Ltac nsatz_internal_discrR ::= discrR.

Require Import Reals.
Require Import RealField.

Lemma Rsth : Setoid_Theory R (@eq R).

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

Instance Rri : (Ring (Ro:=Rops)).
Defined.

Class can_compute_Z (z : Z) := dummy_can_compute_Z : True.
Hint Extern 0 (can_compute_Z ?v) =>
  match isZcst v with true => exact I end : typeclass_instances.
Instance reify_IZR z lvar {_ : can_compute_Z z} : reify (PEc z) lvar (IZR z).
Defined.

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

Instance Rcri: (Cring (Rr:=Rri)).


Instance Rdi : (Integral_domain (Rcr:=Rcri)).


Require Import QArith.

Instance Qops: (@Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq).
Defined.

Instance Qri : (Ring (Ro:=Qops)).
Defined.

Lemma Q_one_zero: not (Qeq 1%Q 0%Q).

Instance Qcri: (Cring (Rr:=Qri)).


Instance Qdi : (Integral_domain (Rcr:=Qcri)).


Lemma Z_one_zero: 1%Z <> 0%Z.

Instance Zcri: (Cring (Rr:=Zr)).


Instance Zdi : (Integral_domain (Rcr:=Zcri)).