Library Coq.setoid_ring.Rings_R

Require Export Cring.
Require Export Integral_domain.

Require Import Reals.
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.

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

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

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