The Coq Proof Assistant

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