src/HOL/Power.thy
changeset 65057 799bbbb3a395
parent 64964 a0c985a57f7e
child 66912 a99a7cbf0fb5
     1.1 --- a/src/HOL/Power.thy	Mon Feb 27 00:00:28 2017 +0100
     1.2 +++ b/src/HOL/Power.thy	Mon Feb 27 17:17:26 2017 +0000
     1.3 @@ -563,6 +563,11 @@
     1.4  lemma power_Suc_le_self: "0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ Suc n \<le> a"
     1.5    using power_decreasing [of 1 "Suc n" a] by simp
     1.6  
     1.7 +lemma power2_eq_iff_nonneg [simp]:
     1.8 +  assumes "0 \<le> x" "0 \<le> y"
     1.9 +  shows "(x ^ 2 = y ^ 2) \<longleftrightarrow> x = y"
    1.10 +using assms power2_eq_imp_eq by blast
    1.11 +
    1.12  end
    1.13  
    1.14  context linordered_ring_strict