diff options
Diffstat (limited to 'theories/Numbers/Natural/Binary/NBinDefs.v')
| -rw-r--r-- | theories/Numbers/Natural/Binary/NBinDefs.v | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/theories/Numbers/Natural/Binary/NBinDefs.v b/theories/Numbers/Natural/Binary/NBinDefs.v index c2c7767d5a..c5122ac08e 100644 --- a/theories/Numbers/Natural/Binary/NBinDefs.v +++ b/theories/Numbers/Natural/Binary/NBinDefs.v @@ -31,14 +31,7 @@ Definition NZadd := Nplus. Definition NZsub := Nminus. Definition NZmul := Nmult. -Theorem NZeq_equiv : equiv N NZeq. -Proof (eq_equiv N). - -Add Relation N NZeq - reflexivity proved by (proj1 NZeq_equiv) - symmetry proved by (proj2 (proj2 NZeq_equiv)) - transitivity proved by (proj1 (proj2 NZeq_equiv)) -as NZeq_rel. +Instance NZeq_equiv : Equivalence NZeq. Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd. Proof. |