# HG changeset patch
# User haftmann
# Date 1491982063 -7200
# Node ID 067210a08a220f66230a0894038d19aee2a5f4e2
# Parent  f3cd78ba687c5c9110c1093776e8bfb811593fe1
more fundamental euler's totient function on nat rather than int;
avoid generic name phi;
separate theory for euler's totient function

diff -r f3cd78ba687c -r 067210a08a22 NEWS
--- a/NEWS	Wed Apr 12 13:48:07 2017 +0200
+++ b/NEWS	Wed Apr 12 09:27:43 2017 +0200
@@ -66,6 +66,10 @@
 fps_exp/fps_ln/fps_hypergeo to avoid polluting the name space.
 INCOMPATIBILITY.
 
+* Theory Totient in session Number_Theory introduces basic notions
+about Euler's totient function previously hidden as solitary example
+in theory Residues.  Minor INCOMPATIBILITY.
+
 * Session "Computional_Algebra" covers many previously scattered
 theories, notably Euclidean_Algorithm, Factorial_Ring, Formal_Power_Series,
 Fraction_Field, Fundamental_Theorem_Algebra, Normalized_Fraction,
diff -r f3cd78ba687c -r 067210a08a22 src/HOL/Number_Theory/Euler_Criterion.thy
--- a/src/HOL/Number_Theory/Euler_Criterion.thy	Wed Apr 12 13:48:07 2017 +0200
+++ b/src/HOL/Number_Theory/Euler_Criterion.thy	Wed Apr 12 09:27:43 2017 +0200
@@ -17,17 +17,33 @@
 
 private lemma p_minus_1_int: "int (p - 1) = int p - 1" using p_prime prime_ge_1_nat by force
 
-private lemma E_1: assumes "QuadRes p a"
-  shows "[a ^ ((p - 1) div 2) = 1] (mod (int p))"
+private lemma E_1:
+  assumes "QuadRes (int p) a"
+  shows "[a ^ ((p - 1) div 2) = 1] (mod int p)"
 proof -
-  from assms obtain b where b: "[b ^ 2 = a] (mod p)" unfolding QuadRes_def by blast
-  hence "[a ^ ((p - 1) div 2) = b ^ (2 * ((p - 1) div 2))] (mod p)"
+  from assms obtain b where b: "[b ^ 2 = a] (mod int p)"
+    unfolding QuadRes_def by blast
+  then have "[a ^ ((p - 1) div 2) = b ^ (2 * ((p - 1) div 2))] (mod int p)"
     by (simp add: cong_exp_int cong_sym_int power_mult)
-  hence "[a ^ ((p - 1) div 2) = b ^ (p - 1)] (mod p)" using odd_p by force
-  moreover have "~ p dvd b"
-    using b cong_altdef_int[of a 0 p] cong_dvd_eq_int[of "b ^ 2" a "int p"] p_a_relprime p_prime
-    by (auto simp: prime_dvd_power_int_iff)
-  ultimately show ?thesis using fermat_theorem[of p b] p_prime 
+  then have "[a ^ ((p - 1) div 2) = b ^ (p - 1)] (mod int p)"
+    using odd_p by force
+  moreover have "[b ^ (p - 1) = 1] (mod int p)"
+  proof -
+    have "[nat \<bar>b\<bar> ^ (p - 1) = 1] (mod p)"
+    using p_prime proof (rule fermat_theorem)
+      show "\<not> p dvd nat \<bar>b\<bar>"
+        by (metis b cong_altdef_int cong_dvd_eq_int diff_zero int_dvd_iff p_a_relprime p_prime prime_dvd_power_int_iff prime_nat_int_transfer rel_simps(51))
+    qed
+    then have "nat \<bar>b\<bar> ^ (p - 1) mod p = 1 mod p"
+      by (simp add: cong_nat_def)
+    then have "int (nat \<bar>b\<bar> ^ (p - 1) mod p) = int (1 mod p)"
+      by simp
+    moreover from odd_p have "\<bar>b\<bar> ^ (p - Suc 0) = b ^ (p - Suc 0)"
+      by (simp add: power_even_abs)
+    ultimately show ?thesis
+      by (simp add: zmod_int cong_int_def)
+  qed
+  ultimately show ?thesis
     by (auto intro: cong_trans_int)
 qed
 
diff -r f3cd78ba687c -r 067210a08a22 src/HOL/Number_Theory/Pocklington.thy
--- a/src/HOL/Number_Theory/Pocklington.thy	Wed Apr 12 13:48:07 2017 +0200
+++ b/src/HOL/Number_Theory/Pocklington.thy	Wed Apr 12 09:27:43 2017 +0200
@@ -115,46 +115,6 @@
 
 subsection\<open>Lucas's theorem\<close>
 
-lemma phi_limit_strong: "phi(n) \<le> n - 1"
-proof -
-  have "phi n = card {x. 0 < x \<and> x < int n \<and> coprime x (int n)}"
-    by (simp add: phi_def)
-  also have "... \<le> card {0 <..< int n}"
-    by (rule card_mono) auto
-  also have "... = card {0 <..< n}"
-    by (simp add: transfer_nat_int_set_functions)
-  also have "... \<le> n - 1"
-    by (metis card_greaterThanLessThan le_refl One_nat_def)
-  finally show ?thesis .
-qed
-
-lemma phi_lowerbound_1: assumes n: "n \<ge> 2"
-  shows "phi n \<ge> 1"
-proof -
-  have "finite {x. 0 < x \<and> x < n}"
-    by simp
-  then have "finite {x. 0 < x \<and> x < n \<and> coprime x n}"
-    by (auto intro: rev_finite_subset)
-  moreover have "{0::int <.. 1} \<subseteq> {x. 0 < x \<and> x < n \<and> coprime x n}"
-    using n by (auto simp add: antisym_conv) 
-  ultimately have "card {0::int <.. 1} \<le> card {x. 0 < x \<and> x < n \<and> coprime x n}"
-    by (rule card_mono)
-  also have "... = phi n"
-    by (simp add: phi_def)
-  finally show ?thesis
-    by simp
-qed
-
-lemma phi_lowerbound_1_nat: assumes n: "n \<ge> 2"
-  shows "phi(int n) \<ge> 1"
-by (metis n nat_le_iff nat_numeral phi_lowerbound_1)
-
-lemma euler_theorem_nat:
-  fixes m::nat 
-  assumes "coprime a m"
-  shows "[a ^ phi m = 1] (mod m)"
-by (metis assms le0 euler_theorem [transferred])
-
 lemma lucas_coprime_lemma:
   fixes n::nat 
   assumes m: "m\<noteq>0" and am: "[a^m = 1] (mod n)"
@@ -181,22 +141,21 @@
 
 lemma lucas_weak:
   fixes n::nat 
-  assumes n: "n \<ge> 2" and an:"[a^(n - 1) = 1] (mod n)"
-  and nm: "\<forall>m. 0 <m \<and> m < n - 1 \<longrightarrow> \<not> [a^m = 1] (mod n)"
+  assumes n: "n \<ge> 2" and an: "[a ^ (n - 1) = 1] (mod n)"
+  and nm: "\<forall>m. 0 < m \<and> m < n - 1 \<longrightarrow> \<not> [a ^ m = 1] (mod n)"
   shows "prime n"
-proof-
-  from n have n1: "n \<noteq> 1" "n\<noteq>0" "n - 1 \<noteq> 0" "n - 1 > 0" "n - 1 < n" by arith+
-  from lucas_coprime_lemma[OF n1(3) an] have can: "coprime a n" .
-  from euler_theorem_nat[OF can] have afn: "[a ^ phi n = 1] (mod n)"
-    by auto 
-  {assume "phi n \<noteq> n - 1"
-    with phi_limit_strong phi_lowerbound_1_nat [OF n]
-    have c:"phi n > 0 \<and> phi n < n - 1"
-      by (metis gr0I leD less_linear not_one_le_zero)
-    from nm[rule_format, OF c] afn have False ..}
-  hence "phi n = n - 1" by blast
-  with prime_phi phi_prime n1(1,2) show ?thesis
-    by auto
+using \<open>n \<ge> 2\<close> proof (rule totient_prime)
+  show "totient n = n - 1"
+  proof (rule ccontr)
+    have "[a ^ totient n = 1] (mod n)"
+      by (rule euler_theorem, rule lucas_coprime_lemma [of "n - 1"])
+        (use n an in auto)
+    moreover assume "totient n \<noteq> n - 1"
+    then have "totient n > 0 \<and> totient n < n - 1"
+      using \<open>n \<ge> 2\<close> by (simp add: order_less_le)
+    ultimately show False
+      using nm by auto
+  qed
 qed
 
 lemma nat_exists_least_iff: "(\<exists>(n::nat). P n) \<longleftrightarrow> (\<exists>n. P n \<and> (\<forall>m < n. \<not> P m))"
@@ -287,15 +246,22 @@
   let ?P = "\<lambda>d. 0 < d \<and> [a ^ d = 1] (mod n)"
   from bigger_prime[of a] obtain p where p: "prime p" "a < p" by blast
   from assms have o: "ord n a = Least ?P" by (simp add: ord_def)
-  {assume "n=0 \<or> n=1" with assms have "\<exists>m>0. ?P m" 
-      by auto}
-  moreover
-  {assume "n\<noteq>0 \<and> n\<noteq>1" hence n2:"n \<ge> 2" by arith
-    from assms have na': "coprime a n"
-      by (metis gcd.commute)
-    from phi_lowerbound_1_nat[OF n2] euler_theorem_nat [OF na']
-    have ex: "\<exists>m>0. ?P m" by - (rule exI[where x="phi n"], auto) }
-  ultimately have ex: "\<exists>m>0. ?P m" by blast
+  have ex: "\<exists>m>0. ?P m"
+  proof (cases "n \<ge> 2")
+    case True
+    moreover from assms have "coprime a n"
+      by (simp add: ac_simps)
+    then have "[a ^ totient n = 1] (mod n)"
+      by (rule euler_theorem)
+    ultimately show ?thesis
+      by (auto intro: exI [where x = "totient n"])
+  next
+    case False
+    then have "n = 0 \<or> n = 1"
+      by auto
+    with assms show ?thesis
+      by auto
+  qed
   from nat_exists_least_iff'[of ?P] ex assms show ?thesis
     unfolding o[symmetric] by auto
 qed
@@ -384,9 +350,9 @@
   ultimately  show ?rhs by blast
 qed
 
-lemma order_divides_phi: 
-  fixes n::nat shows "coprime n a \<Longrightarrow> ord n a dvd phi n"
-  by (metis ord_divides euler_theorem_nat gcd.commute)
+lemma order_divides_totient:
+  "ord n a dvd totient n" if "coprime n a"
+  by (metis euler_theorem gcd.commute ord_divides that)
 
 lemma order_divides_expdiff:
   fixes n::nat and a::nat assumes na: "coprime n a"
@@ -561,7 +527,8 @@
       by auto}
   hence d1: "d = 1" by blast
   hence o: "ord p (a^r) = q" using d by simp
-  from pp phi_prime[of p] have phip: "phi p = p - 1" by simp
+  from pp prime_totient [of p]
+  have totient_eq: "totient p = p - 1" by simp
   {fix d assume d: "d dvd p" "d dvd a" "d \<noteq> 1"
     from pp[unfolded prime_nat_iff] d have dp: "d = p" by blast
     from n have "n \<noteq> 0" by simp
@@ -570,7 +537,7 @@
   hence cpa: "coprime p a" by auto
   have arp: "coprime (a^r) p"
     by (metis coprime_exp cpa gcd.commute) 
-  from euler_theorem_nat[OF arp, simplified ord_divides] o phip
+  from euler_theorem [OF arp, simplified ord_divides] o totient_eq
   have "q dvd (p - 1)" by simp
   then obtain d where d:"p - 1 = q * d" 
     unfolding dvd_def by blast
diff -r f3cd78ba687c -r 067210a08a22 src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Wed Apr 12 13:48:07 2017 +0200
+++ b/src/HOL/Number_Theory/Residues.thy	Wed Apr 12 09:27:43 2017 +0200
@@ -14,6 +14,7 @@
   "~~/src/HOL/Algebra/More_Ring"
   "~~/src/HOL/Algebra/More_Finite_Product"
   "~~/src/HOL/Algebra/Multiplicative_Group"
+  Totient
 begin
 
 definition QuadRes :: "int \<Rightarrow> int \<Rightarrow> bool" where
@@ -244,129 +245,63 @@
 
 subsection \<open>Euler's theorem\<close>
 
-text \<open>The definition of the totient function.\<close>
-
-definition phi :: "int \<Rightarrow> nat"
-  where "phi m = card {x. 0 < x \<and> x < m \<and> coprime x m}"
-
-lemma phi_def_nat: "phi m = card {x. 0 < x \<and> x < nat m \<and> coprime x (nat m)}"
-  unfolding phi_def
-proof (rule bij_betw_same_card [of nat])
-  show "bij_betw nat {x. 0 < x \<and> x < m \<and> coprime x m} {x. 0 < x \<and> x < nat m \<and> coprime x (nat m)}"
-    apply (auto simp add: inj_on_def bij_betw_def image_def)
-     apply (metis dual_order.irrefl dual_order.strict_trans leI nat_1 transfer_nat_int_gcd(1))
-    apply (metis One_nat_def of_nat_0 of_nat_1 of_nat_less_0_iff int_nat_eq nat_int
-        transfer_int_nat_gcd(1) of_nat_less_iff)
-    done
-qed
-  
-lemma prime_phi:
-  assumes "2 \<le> p" "phi p = p - 1"
-  shows "prime p"
+lemma (in residues) totient_eq:
+  "totient (nat m) = card (Units R)"
 proof -
-  have *: "{x. 0 < x \<and> x < p \<and> coprime x p} = {1..p - 1}"
-    using assms unfolding phi_def_nat
-    by (intro card_seteq) fastforce+
-  have False if **: "1 < x" "x < p" and "x dvd p" for x :: nat
-  proof -
-    from * have cop: "x \<in> {1..p - 1} \<Longrightarrow> coprime x p"
-      by blast
-    have "coprime x p"
-      apply (rule cop)
-      using ** apply auto
-      done
-    with \<open>x dvd p\<close> \<open>1 < x\<close> show ?thesis
-      by auto
-  qed
-  then show ?thesis
-    using \<open>2 \<le> p\<close>
-    by (simp add: prime_nat_iff)
-       (metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0
-              not_numeral_le_zero one_dvd)
+  have *: "inj_on nat (Units R)"
+    by (rule inj_onI) (auto simp add: res_units_eq)
+  have "totatives (nat m) = nat ` Units R"
+    by (auto simp add: res_units_eq totatives_def transfer_nat_int_gcd(1))
+      (smt One_nat_def image_def mem_Collect_eq nat_0 nat_eq_iff nat_less_iff of_nat_1 transfer_int_nat_gcd(1))
+  then have "card (totatives (nat m)) = card (nat ` Units R)"
+    by simp
+  also have "\<dots> = card (Units R)"
+    using * card_image [of nat "Units R"] by auto
+  finally show ?thesis
+    by simp
 qed
 
-lemma phi_zero [simp]: "phi 0 = 0"
-  unfolding phi_def by (auto simp add: card_eq_0_iff)
-
-lemma phi_one [simp]: "phi 1 = 0"
-  by (auto simp add: phi_def card_eq_0_iff)
+lemma (in residues_prime) totient_eq: "totient p = p - 1"
+  using totient_eq by (simp add: res_prime_units_eq)
 
-lemma phi_leq: "phi x \<le> nat x - 1"
-proof -
-  have "phi x \<le> card {1..x - 1}"
-    unfolding phi_def by (rule card_mono) auto
-  then show ?thesis by simp
-qed
-
-lemma phi_nonzero:
-  "phi x > 0" if "2 \<le> x"
+lemma (in residues) euler_theorem:
+  assumes "coprime a m"
+  shows "[a ^ totient (nat m) = 1] (mod m)"
 proof -
-  have "finite {y. 0 < y \<and> y < x}"
-    by simp
-  then have "finite {y. 0 < y \<and> y < x \<and> coprime y x}"
-    by (auto intro: rev_finite_subset)
-  moreover have "1 \<in> {y. 0 < y \<and> y < x \<and> coprime y x}"
-    using that by simp
-  ultimately have "card {y. 0 < y \<and> y < x \<and> coprime y x} \<noteq> 0"
-    by auto
-  then show ?thesis
-    by (simp add: phi_def)
-qed
-
-lemma (in residues) phi_eq: "phi m = card (Units R)"
-  by (simp add: phi_def res_units_eq)
-
-lemma (in residues) euler_theorem1:
-  assumes a: "gcd a m = 1"
-  shows "[a^phi m = 1] (mod m)"
-proof -
-  have "a ^ phi m mod m = 1 mod m"
-    by (metis assms finite_Units m_gt_one mod_in_res_units one_cong phi_eq pow_cong units_power_order_eq_one)
+  have "a ^ totient (nat m) mod m = 1 mod m"
+    by (metis assms finite_Units m_gt_one mod_in_res_units one_cong totient_eq pow_cong units_power_order_eq_one)
   then show ?thesis
     using res_eq_to_cong by blast
 qed
 
-text \<open>Outside the locale, we can relax the restriction \<open>m > 1\<close>.\<close>
 lemma euler_theorem:
-  assumes "m \<ge> 0"
-    and "gcd a m = 1"
-  shows "[a^phi m = 1] (mod m)"
+  fixes a m :: nat
+  assumes "coprime a m"
+  shows "[a ^ totient m = 1] (mod m)"
 proof (cases "m = 0 | m = 1")
   case True
   then show ?thesis by auto
 next
   case False
   with assms show ?thesis
-    by (intro residues.euler_theorem1, unfold residues_def, auto)
+    using residues.euler_theorem [of "int m" "int a"] transfer_int_nat_cong
+    by (auto simp add: residues_def transfer_int_nat_gcd(1)) force
 qed
 
-lemma (in residues_prime) phi_prime: "phi p = nat p - 1"
-  by (simp add: residues.phi_eq residues_axioms residues_prime.res_prime_units_eq residues_prime_axioms)
-
-lemma phi_prime: "prime (int p) \<Longrightarrow> phi p = nat p - 1"
-  by (simp add: residues_prime.intro residues_prime.phi_prime)
-
 lemma fermat_theorem:
-  fixes a :: int
-  assumes "prime (int p)"
-    and "\<not> p dvd a"
-  shows "[a^(p - 1) = 1] (mod p)"
+  fixes p a :: nat
+  assumes "prime p" and "\<not> p dvd a"
+  shows "[a ^ (p - 1) = 1] (mod p)"
 proof -
-  from assms have "[a ^ phi p = 1] (mod p)"
-    by (auto intro!: euler_theorem intro!: prime_imp_coprime_int[of p]
-             simp: gcd.commute[of _ "int p"])
-  also have "phi p = nat p - 1"
-    by (rule phi_prime) (rule assms)
-  finally show ?thesis
-    by (metis nat_int)
+  from assms prime_imp_coprime [of p a] have "coprime a p"
+    by (auto simp add: ac_simps)
+  then have "[a ^ totient p = 1] (mod p)"
+     by (rule euler_theorem)
+  also have "totient p = p - 1"
+    by (rule prime_totient) (rule assms)
+  finally show ?thesis .
 qed
 
-lemma fermat_theorem_nat:
-  assumes "prime (int p)" and "\<not> p dvd a"
-  shows "[a ^ (p - 1) = 1] (mod p)"
-  using fermat_theorem [of p a] assms
-  by (metis of_nat_1 of_nat_power transfer_int_nat_cong zdvd_int)
-
 
 subsection \<open>Wilson's theorem\<close>
 
diff -r f3cd78ba687c -r 067210a08a22 src/HOL/Number_Theory/Totient.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Number_Theory/Totient.thy	Wed Apr 12 09:27:43 2017 +0200
@@ -0,0 +1,164 @@
+(*  Title:      HOL/Number_Theory/Totient.thy
+    Author:     Jeremy Avigad
+    Author:     Florian Haftmann
+*)
+
+section \<open>Fundamental facts about Euler's totient function\<close>
+
+theory Totient
+imports
+  "~~/src/HOL/Computational_Algebra/Primes"
+begin
+
+definition totatives :: "nat \<Rightarrow> nat set"
+  where "totatives n = {m. 0 < m \<and> m < n \<and> coprime m n}"
+
+lemma in_totatives_iff [simp]:
+  "m \<in> totatives n \<longleftrightarrow> 0 < m \<and> m < n \<and> coprime m n"
+  by (simp add: totatives_def)
+
+lemma finite_totatives [simp]:
+  "finite (totatives n)"
+  by (simp add: totatives_def)
+
+lemma totatives_subset:
+  "totatives n \<subseteq> {1..<n}"
+  by auto
+
+lemma totatives_subset_Suc_0 [simp]:
+  "totatives n \<subseteq> {Suc 0..<n}"
+  using totatives_subset [of n] by simp
+
+lemma totatives_0 [simp]:
+  "totatives 0 = {}"
+  using totatives_subset [of 0] by simp
+
+lemma totatives_1 [simp]:
+  "totatives 1 = {}"
+  using totatives_subset [of 1] by simp
+
+lemma totatives_Suc_0 [simp]:
+  "totatives (Suc 0) = {}"
+  using totatives_1 by simp
+
+lemma one_in_totatives:
+  assumes "n \<ge> 2"
+  shows "1 \<in> totatives n"
+  using assms by simp
+
+lemma minus_one_in_totatives:
+  assumes "n \<ge> 2"
+  shows "n - 1 \<in> totatives n"
+  using assms coprime_minus_one_nat [of n] by simp
+
+lemma totatives_eq_empty_iff [simp]:
+  "totatives n = {} \<longleftrightarrow> n \<in> {0, 1}"
+proof
+  assume "totatives n = {}"
+  show "n \<in> {0, 1}"
+  proof (rule ccontr)
+    assume "n \<notin> {0, 1}"
+    then have "n \<ge> 2"
+      by simp
+    then have "1 \<in> totatives n"
+      by (rule one_in_totatives)
+    with \<open>totatives n = {}\<close> show False
+      by simp
+  qed
+qed auto
+
+lemma prime_totatives:
+  assumes "prime p"
+  shows "totatives p = {1..<p}"
+proof
+  show "{1..<p} \<subseteq> totatives p"
+  proof
+    fix n
+    assume "n \<in> {1..<p}"
+    with nat_dvd_not_less have "\<not> p dvd n"
+      by auto
+    with assms prime_imp_coprime [of p n] have "coprime p n"
+      by simp
+    with \<open>n \<in> {1..<p}\<close> show "n \<in> totatives p"
+      by (auto simp add: totatives_def ac_simps)
+  qed
+qed auto
+
+lemma totatives_prime:
+  assumes "p \<ge> 2" and "totatives p = {1..<p}"
+  shows "prime p"
+proof (rule ccontr)
+  from \<open>2 \<le> p\<close> have "1 < p"
+    by simp
+  moreover assume "\<not> prime p"
+  ultimately obtain n where "1 < n" "n < p" "n dvd p"
+    by (auto simp add: prime_nat_iff)
+      (metis Suc_lessD Suc_lessI dvd_imp_le dvd_pos_nat le_neq_implies_less)
+  then have "n \<in> {1..<p}"
+    by simp
+  with assms have "n \<in> totatives p"
+    by simp
+  then have "coprime n p"
+    by simp
+  with \<open>1 < n\<close> \<open>n dvd p\<close> show False
+    by simp
+qed
+
+definition totient :: "nat \<Rightarrow> nat"
+  where "totient = card \<circ> totatives"
+
+lemma card_totatives [simp]:
+  "card (totatives n) = totient n"
+  by (simp add: totient_def)
+
+lemma totient_0 [simp]:
+  "totient 0 = 0"
+  by (simp add: totient_def)
+
+lemma totient_1 [simp]:
+  "totient 1 = 0"
+  by (simp add: totient_def)
+
+lemma totient_Suc_0 [simp]:
+  "totient (Suc 0) = 0"
+  using totient_1 by simp
+  
+lemma prime_totient:
+  assumes "prime p"
+  shows "totient p = p - 1"
+  using assms prime_totatives
+  by (simp add: totient_def)
+
+lemma totient_eq_0_iff [simp]:
+  "totient n = 0 \<longleftrightarrow> n \<in> {0, 1}"
+  by (simp only: totient_def comp_def card_eq_0_iff) auto
+
+lemma totient_noneq_0_iff [simp]:
+  "totient n > 0 \<longleftrightarrow> 2 \<le> n"
+proof -
+  have "totient n > 0 \<longleftrightarrow> totient n \<noteq> 0"
+    by blast
+  also have "\<dots> \<longleftrightarrow> 2 \<le> n"
+    by auto
+  finally show ?thesis .
+qed
+
+lemma totient_less_eq:
+  "totient n \<le> n - 1"
+  using card_mono [of "{1..<n}" "totatives n"] by auto
+
+lemma totient_less_eq_Suc_0 [simp]:
+  "totient n \<le> n - Suc 0"
+  using totient_less_eq [of n] by simp
+
+lemma totient_prime:
+  assumes "2 \<le> p" "totient p = p - 1"
+  shows "prime p"
+proof -
+  have "totatives p = {1..<p}"
+    by (rule card_subset_eq) (simp_all add: assms)
+  with assms show ?thesis
+    by (auto intro: totatives_prime)
+qed
+
+end