add lemma power2_eq_iff
authorhuffman
Sat Aug 20 09:59:28 2011 -0700 (2011-08-20)
changeset 44345881c324470a2
parent 44344 49be3e7d4762
child 44346 00dd3c4dabe0
add lemma power2_eq_iff
src/HOL/Nat_Numeral.thy
     1.1 --- a/src/HOL/Nat_Numeral.thy	Sat Aug 20 07:09:44 2011 -0700
     1.2 +++ b/src/HOL/Nat_Numeral.thy	Sat Aug 20 09:59:28 2011 -0700
     1.3 @@ -129,6 +129,14 @@
     1.4  
     1.5  end
     1.6  
     1.7 +context idom
     1.8 +begin
     1.9 +
    1.10 +lemma power2_eq_iff: "x\<twosuperior> = y\<twosuperior> \<longleftrightarrow> x = y \<or> x = - y"
    1.11 +  unfolding power2_eq_square by (rule square_eq_iff)
    1.12 +
    1.13 +end
    1.14 +
    1.15  context linordered_ring
    1.16  begin
    1.17