equal
deleted
inserted
replaced
607 |
607 |
608 end |
608 end |
609 |
609 |
610 |
610 |
611 subsection {* Miscellaneous rules *} |
611 subsection {* Miscellaneous rules *} |
|
612 |
|
613 lemma self_le_power: |
|
614 fixes x::"'a::linordered_semidom" |
|
615 shows "1 \<le> x \<Longrightarrow> 0 < n \<Longrightarrow> x \<le> x ^ n" |
|
616 by (metis gr_implies_not0 le_eq_less_or_eq less_one nat_le_linear power_increasing power_one_right) |
612 |
617 |
613 lemma power_eq_if: "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))" |
618 lemma power_eq_if: "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))" |
614 unfolding One_nat_def by (cases m) simp_all |
619 unfolding One_nat_def by (cases m) simp_all |
615 |
620 |
616 lemma power2_sum: |
621 lemma power2_sum: |