Library Coq.setoid_ring.Rings_Q

Require Export Cring.
Require Export Integral_domain.

Require Import QArith.

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

#[global]
Instance Qri : (Ring (Ro:=Qops)).
Defined.

#[global]
Instance Qcri: (Cring (Rr:=Qri)).


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

#[global]
Instance Qdi : (Integral_domain (Rcr:=Qcri)).