# HG changeset patch
# User nipkow
# Date 1400594356 -7200
# Node ID 842bb6d362639944684aa21467d18d619552777a
# Parent  b7999893ffcce9eff092d66553d4cbb92c823185
added lemma

diff -r b7999893ffcc -r 842bb6d36263 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue May 20 09:57:10 2014 +0200
+++ b/src/HOL/Nat.thy	Tue May 20 15:59:16 2014 +0200
@@ -870,6 +870,10 @@
   then show "P n" by auto
 qed
 
+
+lemma Least_eq_0[simp]: "P(0::nat) \<Longrightarrow> Least P = 0"
+by (rule Least_equality[OF _ le0])
+
 lemma Least_Suc:
      "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
   apply (cases n, auto)