1 files changed, 0 insertions, 40 deletions
diff --git a/theories/nsatz/Nsatz.v b/theories/nsatz/Nsatz.v
index 70180f47c7..b684775bb4 100644
--- a/theories/nsatz/Nsatz.v
+++ b/theories/nsatz/Nsatz.v
@@ -75,43 +75,3 @@ red. exact Rmult_comm. Defined.
 Instance Rdi : (Integral_domain (Rcr:=Rcri)).
 constructor.
 exact Rmult_integral. exact R_one_zero. Defined.
-
-(* Rational numbers *)
-Require Import QArith.
-
-Instance Qops: (@Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq).
-Defined.
-
-Instance Qri : (Ring (Ro:=Qops)).
-constructor.
-try apply Q_Setoid.
-apply Qplus_comp.
-apply Qmult_comp.
-apply Qminus_comp.
-apply Qopp_comp.
- exact Qplus_0_l. exact Qplus_comm. apply Qplus_assoc.
- exact Qmult_1_l.  exact Qmult_1_r. apply Qmult_assoc.
- apply Qmult_plus_distr_l.  intros. apply Qmult_plus_distr_r.
-reflexivity. exact Qplus_opp_r.
-Defined.
-
-Lemma Q_one_zero: not (Qeq 1%Q 0%Q).
-Proof. unfold Qeq. simpl. lia.  Qed.
-
-Instance Qcri: (Cring (Rr:=Qri)).
-red. exact Qmult_comm. Defined.
-
-Instance Qdi : (Integral_domain (Rcr:=Qcri)).
-constructor.
-exact Qmult_integral. exact Q_one_zero. Defined.
-
-(* Integers *)
-Lemma Z_one_zero: 1%Z <> 0%Z.
-Proof. lia. Qed.
-
-Instance Zcri: (Cring (Rr:=Zr)).
-red. exact Z.mul_comm. Defined.
-
-Instance Zdi : (Integral_domain (Rcr:=Zcri)).
-constructor.
-exact Zmult_integral. exact Z_one_zero. Defined.