diff options
| -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 *) |