src/HOL/Nat.thy

--- 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>