# HG changeset patch
# User nipkow
# Date 1479836219 -3600
# Node ID e44f5c123f2667787c9df0694aabca060249665a
# Parent  ec766f7b887ec63ade54669b4137e1bae90596b7
added lemma

diff -r ec766f7b887e -r e44f5c123f26 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Nov 22 16:22:05 2016 +0100
+++ b/src/HOL/Nat.thy	Tue Nov 22 18:36:59 2016 +0100
@@ -10,7 +10,7 @@
 section \<open>Natural numbers\<close>
 
 theory Nat
-  imports Inductive Typedef Fun Rings
+imports Inductive Typedef Fun Rings
 begin
 
 named_theorems arith "arith facts -- only ground formulas"
@@ -742,6 +742,8 @@
 lemma less_Suc_eq_0_disj: "m < Suc n \<longleftrightarrow> m = 0 \<or> (\<exists>j. m = Suc j \<and> j < n)"
   by (cases m) simp_all
 
+lemma All_less_Suc: "(\<forall>i < Suc n. P i) = (P n \<and> (\<forall>i < n. P i))"
+by (auto simp: less_Suc_eq)
 
 subsubsection \<open>Monotonicity of Addition\<close>