diff -r 47258727fa42 -r ae2528273eeb src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Tue Sep 17 12:36:04 2019 +0100
+++ b/src/HOL/NthRoot.thy	Tue Sep 17 16:21:31 2019 +0100
@@ -268,10 +268,10 @@
   with assms show ?thesis by simp
 qed
 
-lemma real_root_decreasing: "0 < n \<Longrightarrow> n < N \<Longrightarrow> 1 \<le> x \<Longrightarrow> root N x \<le> root n x"
+lemma real_root_decreasing: "0 < n \<Longrightarrow> n \<le> N \<Longrightarrow> 1 \<le> x \<Longrightarrow> root N x \<le> root n x"
   by (auto simp add: order_le_less real_root_strict_decreasing)
 
-lemma real_root_increasing: "0 < n \<Longrightarrow> n < N \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> root n x \<le> root N x"
+lemma real_root_increasing: "0 < n \<Longrightarrow> n \<le> N \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> root n x \<le> root N x"
   by (auto simp add: order_le_less real_root_strict_increasing)