src/HOL/NthRoot.thy

   from assms have "root N (root n x) ^ N < root n (root N x) ^ n"
     by (simp add: real_root_commute power_strict_decreasing del: real_root_pow_pos2)
   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)
 
 
 text \<open>Continuity and derivatives.\<close>