Library Coq.setoid_ring.Rings_Q

Require Export Cring.
Require Export Integral_domain.

Require Import QArith.

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

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

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


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

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