[STATEMENT]
lemma pow_pref_root_one: assumes "k \<noteq> 0" and "r \<noteq> \<epsilon>" and "r\<^sup>@k \<le>p r"
  shows  "k = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k = 1
[PROOF STEP]
unfolding eq_pow_exp[OF \<open>r \<noteq> \<epsilon>\<close>, of k 1, symmetric] pow_one'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<^sup>@ k = r
[PROOF STEP]
using \<open>r\<^sup>@k \<le>p r\<close> triv_pref[of r "r\<^sup>@(k-1)", folded pop_pow_one[OF \<open>k \<noteq> 0\<close>]]
[PROOF STATE]
proof (prove)
using this:
r \<^sup>@ k \<le>p r
r \<le>p r \<^sup>@ k

goal (1 subgoal):
 1. r \<^sup>@ k = r
[PROOF STEP]
by auto