--- a/src/HOL/Analysis/Tagged_Division.thy Mon Jul 24 16:50:46 2017 +0100
+++ b/src/HOL/Analysis/Tagged_Division.thy Wed Jul 26 13:36:36 2017 +0100
@@ -71,14 +71,6 @@
by (simp add: field_simps)
qed
-declare norm_triangle_ineq4[intro]
-
-lemma transitive_stepwise_le:
- assumes "m \<le> n" "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" and "\<And>n. R n (Suc n)"
- shows "R m n"
-using \<open>m \<le> n\<close>
- by (induction rule: dec_induct) (use assms in blast)+
-
subsection \<open>Some useful lemmas about intervals.\<close>
lemma interior_subset_union_intervals:
--- a/src/HOL/Nat.thy Mon Jul 24 16:50:46 2017 +0100
+++ b/src/HOL/Nat.thy Wed Jul 26 13:36:36 2017 +0100
@@ -2143,6 +2143,12 @@
qed
qed
+lemma transitive_stepwise_le:
+ assumes "m \<le> n" "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" and "\<And>n. R n (Suc n)"
+ shows "R m n"
+using \<open>m \<le> n\<close>
+ by (induction rule: dec_induct) (use assms in blast)+
+
subsubsection \<open>Greatest operator\<close>