Update on Numbers; renamed ZOrder.v to ZLt to remove clash with ZArith/Zorder on MacOS.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10323 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 6 deletions

diff --git a/theories/Numbers/Natural/Abstract/NPlus.v b/theories/Numbers/Natural/Abstract/NPlus.v
index a033d95a09..d1269cf03f 100644
--- a/theories/Numbers/Natural/Abstract/NPlus.v
+++ b/theories/Numbers/Natural/Abstract/NPlus.v
@@ -61,7 +61,7 @@ Proof NZplus_cancel_r.
 
 (** Theorems that are valid for natural numbers but cannot be proved for Z *)
 
-Theorem plus_eq_0 : forall n m : N, n + m == 0 <-> n == 0 /\ m == 0.
+Theorem eq_plus_0 : forall n m : N, n + m == 0 <-> n == 0 /\ m == 0.
 Proof.
 intros n m; induct n.
 (* The next command does not work with the axiom plus_0_l from NPlusSig *)
@@ -73,7 +73,7 @@ setoid_replace (S n == 0) with False using relation iff by
  (apply -> neg_false; apply neq_succ_0). tauto.
 Qed.
 
-Theorem plus_eq_succ :
+Theorem eq_plus_succ :
   forall n m : N, (exists p : N, n + m == S p) <->
                     (exists n' : N, n == S n') \/ (exists m' : N, m == S m').
 Proof.
@@ -88,16 +88,16 @@ left; now exists n.
 exists (n + m); now rewrite plus_succ_l.
 Qed.
 
-Theorem plus_eq_1 : forall n m : N,
+Theorem eq_plus_1 : forall n m : N,
   n + m == 1 -> n == 1 /\ m == 0 \/ n == 0 /\ m == 1.
 Proof.
 intros n m H.
 assert (H1 : exists p : N, n + m == S p) by now exists 0.
-apply -> plus_eq_succ in H1. destruct H1 as [[n' H1] | [m' H1]].
+apply -> eq_plus_succ in H1. destruct H1 as [[n' H1] | [m' H1]].
 left. rewrite H1 in H; rewrite plus_succ_l in H; apply succ_inj in H.
-apply -> plus_eq_0 in H. destruct H as [H2 H3]; rewrite H2 in H1; now split.
+apply -> eq_plus_0 in H. destruct H as [H2 H3]; rewrite H2 in H1; now split.
 right. rewrite H1 in H; rewrite plus_succ_r in H; apply succ_inj in H.
-apply -> plus_eq_0 in H. destruct H as [H2 H3]; rewrite H3 in H1; now split.
+apply -> eq_plus_0 in H. destruct H as [H2 H3]; rewrite H3 in H1; now split.
 Qed.
 
 Theorem succ_plus_discr : forall n m : N, m ~= S (n + m).