--- 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>