2357 apply (clarsimp simp add: aibi mult_le_cancel_right divide_le_cancel not_less not_le) |
2357 apply (clarsimp simp add: aibi mult_le_cancel_right divide_le_cancel not_less not_le) |
2358 apply (drule_tac x=i in bspec, assumption) |
2358 apply (drule_tac x=i in bspec, assumption) |
2359 using \<open>m\<le>n\<close> realff [of _ _ "1+_"] realff [of "1+_"_ "1+_"] |
2359 using \<open>m\<le>n\<close> realff [of _ _ "1+_"] realff [of "1+_"_ "1+_"] |
2360 apply (auto simp: divide_simps add.commute not_le nat_le_iff_add realff) |
2360 apply (auto simp: divide_simps add.commute not_le nat_le_iff_add realff) |
2361 apply (simp_all add: power_add) |
2361 apply (simp_all add: power_add) |
2362 apply (metis (no_types, hide_lams) mult_Suc mult_less_cancel2 not_less_eq mult.assoc) |
2362 apply (metis (no_types, opaque_lifting) mult_Suc mult_less_cancel2 not_less_eq mult.assoc) |
2363 apply (metis (no_types, hide_lams) mult_Suc mult_less_cancel2 not_less_eq mult.assoc) |
2363 apply (metis (no_types, opaque_lifting) mult_Suc mult_less_cancel2 not_less_eq mult.assoc) |
2364 done |
2364 done |
2365 then show "?K0(m,v) \<subseteq> ?K0(n,w) \<or> ?K0(n,w) \<subseteq> ?K0(m,v) \<or> interior(?K0(m,v)) \<inter> interior(?K0(n,w)) = {}" |
2365 then show "?K0(m,v) \<subseteq> ?K0(n,w) \<or> ?K0(n,w) \<subseteq> ?K0(m,v) \<or> interior(?K0(m,v)) \<inter> interior(?K0(n,w)) = {}" |
2366 by meson |
2366 by meson |
2367 qed auto |
2367 qed auto |
2368 show "\<And>A B. \<lbrakk>A \<in> ?D0; B \<in> ?D0\<rbrakk> \<Longrightarrow> A \<subseteq> B \<or> B \<subseteq> A \<or> interior A \<inter> interior B = {}" |
2368 show "\<And>A B. \<lbrakk>A \<in> ?D0; B \<in> ?D0\<rbrakk> \<Longrightarrow> A \<subseteq> B \<or> B \<subseteq> A \<or> interior A \<inter> interior B = {}" |