[STATEMENT]
lemma per_drop_exp: "u \<le>p (r\<^sup>@m)\<^sup>\<omega>  \<Longrightarrow> u \<le>p r\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<le>p r \<^sup>@ m\<^sup>\<omega> \<Longrightarrow> u \<le>p r\<^sup>\<omega>
[PROOF STEP]
unfolding per_pref[of u r] per_pref[of u "r\<^sup>@m"] pow_mult[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>k. u \<le>p r \<^sup>@ (m * k)) \<and> r \<^sup>@ m \<noteq> \<epsilon> \<Longrightarrow> (\<exists>k. u \<le>p r \<^sup>@ k) \<and> r \<noteq> \<epsilon>
[PROOF STEP]
using nemp_pow_nemp
[PROOF STATE]
proof (prove)
using this:
?t \<^sup>@ ?m \<noteq> \<epsilon> \<Longrightarrow> ?t \<noteq> \<epsilon>

goal (1 subgoal):
 1. (\<exists>k. u \<le>p r \<^sup>@ (m * k)) \<and> r \<^sup>@ m \<noteq> \<epsilon> \<Longrightarrow> (\<exists>k. u \<le>p r \<^sup>@ k) \<and> r \<noteq> \<epsilon>
[PROOF STEP]
by blast