equal
deleted
inserted
replaced
648 done |
648 done |
649 |
649 |
650 lemma rabs_ratiotest_lemma: "[| c \<le> 0; abs x \<le> c * abs y |] ==> x = (0::real)" |
650 lemma rabs_ratiotest_lemma: "[| c \<le> 0; abs x \<le> c * abs y |] ==> x = (0::real)" |
651 by (erule norm_ratiotest_lemma, simp) |
651 by (erule norm_ratiotest_lemma, simp) |
652 |
652 |
|
653 (* TODO: MOVE *) |
653 lemma le_Suc_ex: "(k::nat) \<le> l ==> (\<exists>n. l = k + n)" |
654 lemma le_Suc_ex: "(k::nat) \<le> l ==> (\<exists>n. l = k + n)" |
654 apply (drule le_imp_less_or_eq) |
655 apply (drule le_imp_less_or_eq) |
655 apply (auto dest: less_imp_Suc_add) |
656 apply (auto dest: less_imp_Suc_add) |
656 done |
657 done |
657 |
658 |