src/HOL/Library/Formal_Power_Series.thy
changeset 29915 2146e512cec9
parent 29914 c9ced4f54e82
child 30273 ecd6f0ca62ea
     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Sat Feb 14 16:51:18 2009 -0800
     1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Sat Feb 14 19:01:31 2009 -0800
     1.3 @@ -691,17 +691,6 @@
     1.4    by (simp_all add: fps_power_def)
     1.5  end
     1.6  
     1.7 -lemma fps_square_eq_iff: "(a:: 'a::idom fps)^ 2 = b^2  \<longleftrightarrow> (a = b \<or> a = -b)"
     1.8 -proof-
     1.9 -  {assume "a = b \<or> a = -b" hence "a^2 = b^2" by auto}
    1.10 -  moreover
    1.11 -  {assume "a^2 = b^2 "
    1.12 -    hence "a^2 - b^2 = 0" by simp
    1.13 -    hence "(a-b) * (a+b) = 0" by (simp add: power2_eq_square ring_simps)
    1.14 -    hence "a = b \<or> a = -b" by (simp add: eq_neg_iff_add_eq_0)}
    1.15 -  ultimately show ?thesis by blast
    1.16 -qed
    1.17 -
    1.18  lemma fps_power_zeroth_eq_one: "a$0 =1 \<Longrightarrow> a^n $ 0 = (1::'a::semiring_1)"
    1.19    by (induct n, auto simp add: fps_power_def expand_fps_eq fps_mult_nth)
    1.20