equal
deleted
inserted
replaced
52 lemma nonpos_Ints_of_int: "n \<le> 0 \<Longrightarrow> of_int n \<in> \<int>\<^sub>\<le>\<^sub>0" |
52 lemma nonpos_Ints_of_int: "n \<le> 0 \<Longrightarrow> of_int n \<in> \<int>\<^sub>\<le>\<^sub>0" |
53 unfolding nonpos_Ints_def by blast |
53 unfolding nonpos_Ints_def by blast |
54 |
54 |
55 lemma nonpos_IntsI: |
55 lemma nonpos_IntsI: |
56 "x \<in> \<int> \<Longrightarrow> x \<le> 0 \<Longrightarrow> (x :: 'a :: linordered_idom) \<in> \<int>\<^sub>\<le>\<^sub>0" |
56 "x \<in> \<int> \<Longrightarrow> x \<le> 0 \<Longrightarrow> (x :: 'a :: linordered_idom) \<in> \<int>\<^sub>\<le>\<^sub>0" |
57 using assms unfolding nonpos_Ints_def Ints_def by auto |
57 unfolding nonpos_Ints_def Ints_def by auto |
58 |
58 |
59 lemma nonpos_Ints_subset_Ints: "\<int>\<^sub>\<le>\<^sub>0 \<subseteq> \<int>" |
59 lemma nonpos_Ints_subset_Ints: "\<int>\<^sub>\<le>\<^sub>0 \<subseteq> \<int>" |
60 unfolding nonpos_Ints_def Ints_def by blast |
60 unfolding nonpos_Ints_def Ints_def by blast |
61 |
61 |
62 lemma nonpos_Ints_nonpos [dest]: "x \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> x \<le> (0 :: 'a :: linordered_idom)" |
62 lemma nonpos_Ints_nonpos [dest]: "x \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> x \<le> (0 :: 'a :: linordered_idom)" |