equal
deleted
inserted
replaced
728 |
728 |
729 lemma power2_nat_le_imp_le: |
729 lemma power2_nat_le_imp_le: |
730 fixes m n :: nat |
730 fixes m n :: nat |
731 assumes "m\<^sup>2 \<le> n" |
731 assumes "m\<^sup>2 \<le> n" |
732 shows "m \<le> n" |
732 shows "m \<le> n" |
733 using assms by (cases m) (simp_all add: power2_eq_square) |
733 proof (cases m) |
734 |
734 case 0 then show ?thesis by simp |
|
735 next |
|
736 case (Suc k) |
|
737 show ?thesis |
|
738 proof (rule ccontr) |
|
739 assume "\<not> m \<le> n" |
|
740 then have "n < m" by simp |
|
741 with assms Suc show False |
|
742 by (auto simp add: algebra_simps) (simp add: power2_eq_square) |
|
743 qed |
|
744 qed |
735 |
745 |
736 |
746 |
737 subsection {* Code generator tweak *} |
747 subsection {* Code generator tweak *} |
738 |
748 |
739 lemma power_power_power [code]: |
749 lemma power_power_power [code]: |