added lemma

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