src/HOL/GCD.thy
changeset 34221 3ae38d4b090c
parent 34030 829eb528b226
child 34222 e33ee7369ecb
equal deleted inserted replaced
34216:ada8eb23a08e 34221:3ae38d4b090c
   876     hence "a'*?g dvd b'*?g" by simp
   876     hence "a'*?g dvd b'*?g" by simp
   877     with ab'(1,2)  have ?thesis by simp }
   877     with ab'(1,2)  have ?thesis by simp }
   878   ultimately show ?thesis by blast
   878   ultimately show ?thesis by blast
   879 qed
   879 qed
   880 
   880 
   881 (* FIXME move to Divides(?) *)
       
   882 lemma pow_divides_eq_nat [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"
   881 lemma pow_divides_eq_nat [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"
   883   by (auto intro: pow_divides_pow_nat dvd_power_same)
   882   by (auto intro: pow_divides_pow_nat dvd_power_same)
   884 
   883 
   885 lemma pow_divides_eq_int [simp]: "n ~= 0 \<Longrightarrow> ((a::int)^n dvd b^n) = (a dvd b)"
   884 lemma pow_divides_eq_int [simp]: "n ~= 0 \<Longrightarrow> ((a::int)^n dvd b^n) = (a dvd b)"
   886   by (auto intro: pow_divides_pow_int dvd_power_same)
   885   by (auto intro: pow_divides_pow_int dvd_power_same)