aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-08-08 23:04:34 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-08-08 23:04:34 +0000
commit9e6e9ccac3ac803229336cdef3b272ea7c857993 (patch)
tree3639a4e8ec74d6d6d06d88c7d563fa149acd3b92 /theories
parent022f78302514e071ca60c2e8719a1e2ec66eaed6 (diff)
Some forgotten lemma in Arith with "O" in the name instead of "0".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14391 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
-rw-r--r--theories/Arith/Lt.v7
1 files changed, 4 insertions, 3 deletions
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index 708cdcbf7..e07bba8d9 100644
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -94,9 +94,9 @@ Proof.
Qed.
Hint Resolve lt_0_Sn: arith v62.
-Theorem lt_n_O : forall n, ~ n < 0.
-Proof le_Sn_O.
-Hint Resolve lt_n_O: arith v62.
+Theorem lt_n_0 : forall n, ~ n < 0.
+Proof le_Sn_0.
+Hint Resolve lt_n_0: arith v62.
(** * Predecessor *)
@@ -190,4 +190,5 @@ Hint Immediate lt_0_neq: arith v62.
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).
+Notation lt_n_O := lt_n_0 (only parsing).
(* end hide *)