src/HOL/Power.thy

      "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x < b ^ y) = (x < y)"
   by (blast intro: power_less_imp_less_exp power_strict_increasing) 
 
 lemma power_le_imp_le_base:
   assumes le: "a ^ Suc n \<le> b ^ Suc n"
-      and xnonneg: "(0::'a::{ordered_semidom,recpower}) \<le> a"
-      and ynonneg: "0 \<le> b"
+      and ynonneg: "(0::'a::{ordered_semidom,recpower}) \<le> b"
   shows "a \<le> b"
  proof (rule ccontr)
    assume "~ a \<le> b"
    then have "b < a" by (simp only: linorder_not_le)
    then have "b ^ Suc n < a ^ Suc n"