src/HOL/GCD.thy
 changeset 34221 3ae38d4b090c parent 34030 829eb528b226 child 34222 e33ee7369ecb
equal inserted replaced
`   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 `
`   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)`