From 9e6e9ccac3ac803229336cdef3b272ea7c857993 Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 8 Aug 2011 23:04:34 +0000 Subject: 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 --- theories/Arith/Lt.v | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'theories/Arith') 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 *) -- cgit v1.2.3