Some lemmas about dependent choice + extensions of Compare_dec +

synonyms in Le.v, Lt.v, Gt.v.

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

1 files changed, 12 insertions, 6 deletions

diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index bdd7ce092..af435e54b 100644
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -90,11 +90,11 @@ Proof.
 Qed.
 Hint Immediate lt_S_n: arith v62.
 
-Theorem lt_O_Sn : forall n, 0 < S n.
+Theorem lt_0_Sn : forall n, 0 < S n.
 Proof.
   auto with arith.
 Qed.
-Hint Resolve lt_O_Sn: arith v62.
+Hint Resolve lt_0_Sn: arith v62.
 
 Theorem lt_n_O : forall n, ~ n < 0.
 Proof le_Sn_O.
@@ -175,15 +175,21 @@ Qed.
 
 (** * Comparison to 0 *)
 
-Theorem neq_O_lt : forall n, 0 <> n -> 0 < n.
+Theorem neq_0_lt : forall n, 0 <> n -> 0 < n.
 Proof.
   induction n; auto with arith.
   intros; absurd (0 = 0); trivial with arith.
 Qed.
-Hint Immediate neq_O_lt: arith v62.
+Hint Immediate neq_0_lt: arith v62.
 
-Theorem lt_O_neq : forall n, 0 < n -> 0 <> n.
+Theorem lt_0_neq : forall n, 0 < n -> 0 <> n.
 Proof.
   induction 1; auto with arith.
 Qed.
-Hint Immediate lt_O_neq: arith v62.
\ No newline at end of file
+Hint Immediate lt_0_neq: arith v62.
+
+(* begin hide *)
+Notation lt_O_Sn := lt_0_Sn (only parsing).
+Notation neq_O_lt := neq_0_lt (only parsing).
+Notation lt_O_neq := lt_0_neq (only parsing).
+(* end hide *)