equal
deleted
inserted
replaced
450 next |
450 next |
451 case False with nonneg have "1 < i" by auto |
451 case False with nonneg have "1 < i" by auto |
452 from power_strict_increasing_iff [OF this] less show ?thesis .. |
452 from power_strict_increasing_iff [OF this] less show ?thesis .. |
453 qed |
453 qed |
454 |
454 |
|
455 lemma power_dvd_imp_le: |
|
456 "i ^ m dvd i ^ n \<Longrightarrow> (1::nat) < i \<Longrightarrow> m \<le> n" |
|
457 apply (rule power_le_imp_le_exp, assumption) |
|
458 apply (erule dvd_imp_le, simp) |
|
459 done |
|
460 |
455 |
461 |
456 subsection {* Code generator tweak *} |
462 subsection {* Code generator tweak *} |
457 |
463 |
458 lemma power_power_power [code, code_unfold, code_inline del]: |
464 lemma power_power_power [code, code_unfold, code_inline del]: |
459 "power = power.power (1::'a::{power}) (op *)" |
465 "power = power.power (1::'a::{power}) (op *)" |