# HG changeset patch
# User huffman
# Date 1179076536 -7200
# Node ID 48dc37776d1eea04b721d97ea728a49cc32f2b90
# Parent  372e3471fca2233a4c0b1a90228341389e3bc18e
add lemma power_eq_imp_eq_base

diff -r 372e3471fca2 -r 48dc37776d1e src/HOL/Power.thy
--- a/src/HOL/Power.thy	Sun May 13 18:16:49 2007 +0200
+++ b/src/HOL/Power.thy	Sun May 13 19:15:36 2007 +0200
@@ -319,6 +319,11 @@
       ==> a = (b::'a::{ordered_semidom,recpower})"
 by (blast intro: power_le_imp_le_base order_antisym order_eq_refl sym)
 
+lemma power_eq_imp_eq_base:
+  fixes a b :: "'a::{ordered_semidom,recpower}"
+  shows "\<lbrakk>a ^ n = b ^ n; 0 \<le> a; 0 \<le> b; 0 < n\<rbrakk> \<Longrightarrow> a = b"
+by (cases n, simp_all, rule power_inject_base)
+
 
 subsection{*Exponentiation for the Natural Numbers*}