equal
deleted
inserted
replaced
3684 by blast |
3684 by blast |
3685 with s_def n0 p_def nb nf have ?ths by auto} |
3685 with s_def n0 p_def nb nf have ?ths by auto} |
3686 ultimately show ?ths by auto |
3686 ultimately show ?ths by auto |
3687 qed |
3687 qed |
3688 next |
3688 next |
3689 case (3 a b) thus ?case by auto |
3689 case (3 a b) then show ?case |
|
3690 apply auto |
|
3691 apply (erule_tac x = "(aa, aaa, ba)" in ballE) apply simp_all |
|
3692 apply (erule_tac x = "(ab, ac, baa)" in ballE) apply simp_all |
|
3693 done |
3690 qed (auto simp add: Let_def split_def ring_simps conj_rl) |
3694 qed (auto simp add: Let_def split_def ring_simps conj_rl) |
3691 |
3695 |
3692 lemma real_in_int_intervals: |
3696 lemma real_in_int_intervals: |
3693 assumes xb: "real m \<le> x \<and> x < real ((n::int) + 1)" |
3697 assumes xb: "real m \<le> x \<and> x < real ((n::int) + 1)" |
3694 shows "\<exists> j\<in> {m.. n}. real j \<le> x \<and> x < real (j+1)" (is "\<exists> j\<in> ?N. ?P j") |
3698 shows "\<exists> j\<in> {m.. n}. real j \<le> x \<and> x < real (j+1)" (is "\<exists> j\<in> ?N. ?P j") |