equal
deleted
inserted
replaced
175 thus ?thesis by (simp add: totient_def) |
175 thus ?thesis by (simp add: totient_def) |
176 qed |
176 qed |
177 |
177 |
178 lemma totient_less: |
178 lemma totient_less: |
179 assumes "n > 1" |
179 assumes "n > 1" |
180 shows "totient n < n" |
180 shows "totient n < n" |
181 proof - |
181 proof - |
182 from assms have "card (totatives n) \<le> card {0<..<n}" |
182 from assms have "card (totatives n) \<le> card {0<..<n}" |
183 using totatives_less[of _ n] totatives_subset[of n] by (intro card_mono) auto |
183 using totatives_less[of _ n] totatives_subset[of n] by (intro card_mono) auto |
184 with assms show ?thesis by (simp add: totient_def) |
184 with assms show ?thesis by (simp add: totient_def) |
185 qed |
185 qed |