src/HOL/Series.thy
changeset 50331 4b6dc5077e98
parent 47761 dfe747e72fa8
child 50999 3de230ed0547
     1.1 --- a/src/HOL/Series.thy	Mon Dec 03 18:19:11 2012 +0100
     1.2 +++ b/src/HOL/Series.thy	Mon Dec 03 18:19:12 2012 +0100
     1.3 @@ -650,6 +650,7 @@
     1.4  lemma rabs_ratiotest_lemma: "[| c \<le> 0; abs x \<le> c * abs y |] ==> x = (0::real)"
     1.5  by (erule norm_ratiotest_lemma, simp)
     1.6  
     1.7 +(* TODO: MOVE *)
     1.8  lemma le_Suc_ex: "(k::nat) \<le> l ==> (\<exists>n. l = k + n)"
     1.9  apply (drule le_imp_less_or_eq)
    1.10  apply (auto dest: less_imp_Suc_add)