aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-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 *)