diff options
Diffstat (limited to 'theories/Numbers/Integer/Abstract')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZAxioms.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZBase.v | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index dfffe9a7f..bd6db10d9 100644 --- a/theories/Numbers/Integer/Abstract/ZAxioms.v +++ b/theories/Numbers/Integer/Abstract/ZAxioms.v @@ -48,7 +48,7 @@ Parameter Zopp : Z -> Z. (*Notation "- 1" := (Zopp 1) : IntScope. Check (-1).*) -Add Morphism Zopp with signature Zeq ==> Zeq as Zopp_wd. +Instance Zopp_wd : Proper (Zeq==>Zeq) Zopp. Notation "- x" := (Zopp x) (at level 35, right associativity) : IntScope. Notation "- 1" := (Zopp (NZsucc NZ0)) : IntScope. diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v index 648cde197..7b3c0ba6e 100644 --- a/theories/Numbers/Integer/Abstract/ZBase.v +++ b/theories/Numbers/Integer/Abstract/ZBase.v @@ -34,13 +34,13 @@ Theorem Zpred_succ : forall n : Z, P (S n) == n. Proof NZpred_succ. Theorem Zeq_refl : forall n : Z, n == n. -Proof (proj1 NZeq_equiv). +Proof (@Equivalence_Reflexive _ _ NZeq_equiv). Theorem Zeq_sym : forall n m : Z, n == m -> m == n. -Proof (proj2 (proj2 NZeq_equiv)). +Proof (@Equivalence_Symmetric _ _ NZeq_equiv). Theorem Zeq_trans : forall n m p : Z, n == m -> m == p -> n == p. -Proof (proj1 (proj2 NZeq_equiv)). +Proof (@Equivalence_Transitive _ _ NZeq_equiv). Theorem Zneq_sym : forall n m : Z, n ~= m -> m ~= n. Proof NZneq_sym. |