src/ZF/Arith.thy

--- a/src/ZF/Arith.thy	Mon Sep 13 09:57:25 2004 +0200
+++ b/src/ZF/Arith.thy	Fri Sep 17 16:08:52 2004 +0200
@@ -307,6 +307,9 @@
 lemma add_lt_elim1: "[| k#+m < k#+n; m \<in> nat; n \<in> nat |] ==> m < n"
 by (drule add_lt_elim1_natify, auto)
 
+lemma zero_less_add: "[| n \<in> nat; m \<in> nat |] ==> 0 < m #+ n <-> (0<m | 0<n)"
+by (induct_tac "n", auto)
+
 
 subsection{*Monotonicity of Addition*}