diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-08-08 23:04:34 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-08-08 23:04:34 +0000 |
| commit | 9e6e9ccac3ac803229336cdef3b272ea7c857993 (patch) | |
| tree | 3639a4e8ec74d6d6d06d88c7d563fa149acd3b92 /theories/Arith | |
| parent | 022f78302514e071ca60c2e8719a1e2ec66eaed6 (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/Arith')
| -rw-r--r-- | theories/Arith/Lt.v | 7 |
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 *) |