diff options
Diffstat (limited to 'theories/Numbers/NatInt/NZAxioms.v')
| -rw-r--r-- | theories/Numbers/NatInt/NZAxioms.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v index 516cf5b42..1ef780986 100644 --- a/theories/Numbers/NatInt/NZAxioms.v +++ b/theories/Numbers/NatInt/NZAxioms.v @@ -20,11 +20,11 @@ Parameter Inline NZ0 : NZ. Parameter Inline NZsucc : NZ -> NZ. Parameter Inline NZpred : NZ -> NZ. Parameter Inline NZadd : NZ -> NZ -> NZ. -Parameter Inline NZminus : NZ -> NZ -> NZ. +Parameter Inline NZsub : NZ -> NZ -> NZ. Parameter Inline NZmul : NZ -> NZ -> NZ. -(* Unary minus (opp) is not defined on natural numbers, so we have it for -integers only *) +(* Unary subtraction (opp) is not defined on natural numbers, so we have + it for integers only *) Axiom NZeq_equiv : equiv NZ NZeq. Add Relation NZ NZeq @@ -36,7 +36,7 @@ as NZeq_rel. Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd. Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd. Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd. -Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd. +Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd. Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd. Delimit Scope NatIntScope with NatInt. @@ -48,7 +48,7 @@ Notation S := NZsucc. Notation P := NZpred. Notation "1" := (S 0) : NatIntScope. Notation "x + y" := (NZadd x y) : NatIntScope. -Notation "x - y" := (NZminus x y) : NatIntScope. +Notation "x - y" := (NZsub x y) : NatIntScope. Notation "x * y" := (NZmul x y) : NatIntScope. Axiom NZpred_succ : forall n : NZ, P (S n) == n. @@ -60,8 +60,8 @@ Axiom NZinduction : Axiom NZadd_0_l : forall n : NZ, 0 + n == n. Axiom NZadd_succ_l : forall n m : NZ, (S n) + m == S (n + m). -Axiom NZminus_0_r : forall n : NZ, n - 0 == n. -Axiom NZminus_succ_r : forall n m : NZ, n - (S m) == P (n - m). +Axiom NZsub_0_r : forall n : NZ, n - 0 == n. +Axiom NZsub_succ_r : forall n m : NZ, n - (S m) == P (n - m). Axiom NZmul_0_l : forall n : NZ, 0 * n == 0. Axiom NZmul_succ_l : forall n m : NZ, S n * m == n * m + m. |