# HG changeset patch
# User nipkow
# Date 1502272876 -7200
# Node ID 962c12353c679549c1135aedfe36f5a71a3d9dab
# Parent  81bc8f4308c187b173fe9e1884f86a2a58982b12
added lemmas

diff -r 81bc8f4308c1 -r 962c12353c67 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Aug 08 23:55:03 2017 +0200
+++ b/src/HOL/Nat.thy	Wed Aug 09 12:01:16 2017 +0200
@@ -764,6 +764,16 @@
 lemma All_less_Suc: "(\<forall>i < Suc n. P i) = (P n \<and> (\<forall>i < n. P i))"
 by (auto simp: less_Suc_eq)
 
+lemma All_less_Suc2: "(\<forall>i < Suc n. P i) = (P 0 \<and> (\<forall>i < n. P(Suc i)))"
+by (auto simp: less_Suc_eq_0_disj)
+
+lemma Ex_less_Suc: "(\<exists>i < Suc n. P i) = (P n \<or> (\<exists>i < n. P i))"
+by (auto simp: less_Suc_eq)
+
+lemma Ex_less_Suc2: "(\<exists>i < Suc n. P i) = (P 0 \<or> (\<exists>i < n. P(Suc i)))"
+by (auto simp: less_Suc_eq_0_disj)
+
+
 subsubsection \<open>Monotonicity of Addition\<close>
 
 lemma Suc_pred [simp]: "n > 0 \<Longrightarrow> Suc (n - Suc 0) = n"