--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Sat Feb 24 17:21:35 2018 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Sun Feb 25 12:54:55 2018 +0000
@@ -158,17 +158,6 @@
using tendsto_cmult_ereal[of c f "f x" "at x within A" for x]
by (auto simp: continuous_on_def simp del: tendsto_cmult_ereal)
-context linordered_nonzero_semiring
-begin
-
-lemma of_nat_nonneg [simp]: "0 \<le> of_nat n"
- by (induct n) simp_all
-
-lemma of_nat_mono[simp]: "i \<le> j \<Longrightarrow> of_nat i \<le> of_nat j"
- by (auto simp add: le_iff_add intro!: add_increasing2)
-
-end
-
lemma real_of_nat_Sup:
assumes "A \<noteq> {}" "bdd_above A"
shows "of_nat (Sup A) = (SUP a:A. of_nat a :: real)"
@@ -181,21 +170,6 @@
by (intro cSUP_upper bdd_above_image_mono assms) (auto simp: mono_def)
qed
-\<comment> \<open>These generalise their counterparts in \<open>Nat.linordered_semidom_class\<close>\<close>
-lemma of_nat_less[simp]:
- "m < n \<Longrightarrow> of_nat m < (of_nat n::'a::{linordered_nonzero_semiring, semiring_char_0})"
- by (auto simp: less_le)
-
-lemma of_nat_le_iff[simp]:
- "of_nat m \<le> (of_nat n::'a::{linordered_nonzero_semiring, semiring_char_0}) \<longleftrightarrow> m \<le> n"
-proof (safe intro!: of_nat_mono)
- assume "of_nat m \<le> (of_nat n::'a)" then show "m \<le> n"
- proof (intro leI notI)
- assume "n < m" from less_le_trans[OF of_nat_less[OF this] \<open>of_nat m \<le> of_nat n\<close>] show False
- by blast
- qed
-qed
-
lemma (in complete_lattice) SUP_sup_const1:
"I \<noteq> {} \<Longrightarrow> (SUP i:I. sup c (f i)) = sup c (SUP i:I. f i)"
using SUP_sup_distrib[of "\<lambda>_. c" I f] by simp