| changeset 73869 | 7181130f5872 |
| parent 73411 | 1f1366966296 |
| child 74438 | 5827b91ef30e |
--- a/src/HOL/Power.thy Wed Jun 23 17:43:31 2021 +0000 +++ b/src/HOL/Power.thy Wed Jun 23 17:43:31 2021 +0000 @@ -908,7 +908,7 @@ lemma power_gt_expt: "n > Suc 0 \<Longrightarrow> n^k > k" by (induction k) (auto simp: less_trans_Suc n_less_m_mult_n) -lemma less_exp: +lemma less_exp [simp]: \<open>n < 2 ^ n\<close> by (simp add: power_gt_expt)