diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-12-12 19:51:03 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-12-12 19:51:03 +0000 |
| commit | 98a86e50e7dc06b77a34bf34a0476aebc07efbcd (patch) | |
| tree | 177e015614f9c5cf3cdf798920322bc888a082d2 /theories/Numbers/Natural/Abstract/NBase.v | |
| parent | a19570bbbe7b42b491eae1cf33ff69a746584235 (diff) | |
Uniformity with the rest of the StdLib : _symm --> _sym
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11675 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Natural/Abstract/NBase.v')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NBase.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index 0d7bc63eb..deee349ca 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -48,14 +48,14 @@ Proof pred_0. Theorem Neq_refl : forall n : N, n == n. Proof (proj1 NZeq_equiv). -Theorem Neq_symm : forall n m : N, n == m -> m == n. +Theorem Neq_sym : forall n m : N, n == m -> m == n. Proof (proj2 (proj2 NZeq_equiv)). Theorem Neq_trans : forall n m p : N, n == m -> m == p -> n == p. Proof (proj1 (proj2 NZeq_equiv)). -Theorem neq_symm : forall n m : N, n ~= m -> m ~= n. -Proof NZneq_symm. +Theorem neq_sym : forall n m : N, n ~= m -> m ~= n. +Proof NZneq_sym. Theorem succ_inj : forall n1 n2 : N, S n1 == S n2 -> n1 == n2. Proof NZsucc_inj. @@ -111,7 +111,7 @@ Qed. Theorem neq_0_succ : forall n : N, 0 ~= S n. Proof. -intro n; apply neq_symm; apply neq_succ_0. +intro n; apply neq_sym; apply neq_succ_0. Qed. (* Next, we show that all numbers are nonnegative and recover regular induction |