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