src/HOL/NewNumberTheory/Cong.thy

+(*  Title:      HOL/Library/Cong.thy
+    ID:         
+    Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
+                Thomas M. Rasmussen, Jeremy Avigad
+
+
+Defines congruence (notation: [x = y] (mod z)) for natural numbers and
+integers.
+
+This file combines and revises a number of prior developments.
+
+The original theories "GCD" and "Primes" were by Christophe Tabacznyj
+and Lawrence C. Paulson, based on \cite{davenport92}. They introduced
+gcd, lcm, and prime for the natural numbers.
+
+The original theory "IntPrimes" was by Thomas M. Rasmussen, and
+extended gcd, lcm, primes to the integers. Amine Chaieb provided
+another extension of the notions to the integers, and added a number
+of results to "Primes" and "GCD". 
+
+The original theory, "IntPrimes", by Thomas M. Rasmussen, defined and
+developed the congruence relations on the integers. The notion was
+extended to the natural numbers by Chiaeb. Jeremy Avigad combined
+these, revised and tidied them, made the development uniform for the
+natural numbers and the integers, and added a number of new theorems.
+
+*)
+
+
+header {* Congruence *}
+
+theory Cong
+imports GCD
+begin
+
+subsection {* Turn off One_nat_def *}
+
+lemma nat_induct' [case_names zero plus1, induct type: nat]: 
+    "\<lbrakk> P (0::nat); !!n. P n \<Longrightarrow> P (n + 1)\<rbrakk> \<Longrightarrow> P n"
+by (erule nat_induct) (simp add:One_nat_def)
+
+lemma nat_cases [case_names zero plus1, cases type: nat]: 
+    "P (0::nat) \<Longrightarrow> (!!n. P (n + 1)) \<Longrightarrow> P n"
+by(metis nat_induct')
+
+lemma power_plus_one [simp]: "(x::'a::power)^(n + 1) = x * x^n"
+by (simp add: One_nat_def)
+
+lemma nat_power_eq_one_eq [simp]: 
+  "((x::nat)^m = 1) = (m = 0 | x = 1)"
+by (induct m, auto)
+
+lemma card_insert_if' [simp]: "finite A \<Longrightarrow>
+  card (insert x A) = (if x \<in> A then (card A) else (card A) + 1)"
+by (auto simp add: insert_absorb)
+
+(* why wasn't card_insert_if a simp rule? *)
+declare card_insert_disjoint [simp del]
+
+lemma nat_1' [simp]: "nat 1 = 1"
+by simp
+
+(* For those annoying moments where Suc reappears *)
+lemma Suc_remove: "Suc n = n + 1"
+by simp
+
+declare nat_1 [simp del]
+declare add_2_eq_Suc [simp del] 
+declare add_2_eq_Suc' [simp del]
+
+
+declare mod_pos_pos_trivial [simp]
+
+
+subsection {* Main definitions *}
+
+class cong =
+
+fixes 
+  cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ = _] '(mod _'))")
+
+begin
+
+abbreviation
+  notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ \<noteq> _] '(mod _'))")
+where
+  "notcong x y m == (~cong x y m)" 
+
+end
+
+(* definitions for the natural numbers *)
+
+instantiation nat :: cong
+
+begin 
+
+definition 
+  cong_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+where 
+  "cong_nat x y m = ((x mod m) = (y mod m))"
+
+instance proof qed
+
+end
+
+
+(* definitions for the integers *)
+
+instantiation int :: cong
+
+begin 
+
+definition 
+  cong_int :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool"
+where 
+  "cong_int x y m = ((x mod m) = (y mod m))"
+
+instance proof qed
+
+end
+
+
+subsection {* Set up Transfer *}
+
+
+lemma transfer_nat_int_cong:
+  "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> m >= 0 \<Longrightarrow> 
+    ([(nat x) = (nat y)] (mod (nat m))) = ([x = y] (mod m))"
+  unfolding cong_int_def cong_nat_def 
+  apply (auto simp add: nat_mod_distrib [symmetric])
+  apply (subst (asm) eq_nat_nat_iff)
+  apply (case_tac "m = 0", force, rule pos_mod_sign, force)+
+  apply assumption
+done
+
+declare TransferMorphism_nat_int[transfer add return: 
+    transfer_nat_int_cong]
+
+lemma transfer_int_nat_cong:
+  "[(int x) = (int y)] (mod (int m)) = [x = y] (mod m)"
+  apply (auto simp add: cong_int_def cong_nat_def)
+  apply (auto simp add: zmod_int [symmetric])
+done
+
+declare TransferMorphism_int_nat[transfer add return: 
+    transfer_int_nat_cong]
+
+
+subsection {* Congruence *}
+
+(* was zcong_0, etc. *)
+lemma nat_cong_0 [simp, presburger]: "([(a::nat) = b] (mod 0)) = (a = b)"
+  by (unfold cong_nat_def, auto)
+
+lemma int_cong_0 [simp, presburger]: "([(a::int) = b] (mod 0)) = (a = b)"
+  by (unfold cong_int_def, auto)
+
+lemma nat_cong_1 [simp, presburger]: "[(a::nat) = b] (mod 1)"
+  by (unfold cong_nat_def, auto)
+
+lemma nat_cong_Suc_0 [simp, presburger]: "[(a::nat) = b] (mod Suc 0)"
+  by (unfold cong_nat_def, auto simp add: One_nat_def)
+
+lemma int_cong_1 [simp, presburger]: "[(a::int) = b] (mod 1)"
+  by (unfold cong_int_def, auto)
+
+lemma nat_cong_refl [simp]: "[(k::nat) = k] (mod m)"
+  by (unfold cong_nat_def, auto)
+
+lemma int_cong_refl [simp]: "[(k::int) = k] (mod m)"
+  by (unfold cong_int_def, auto)
+
+lemma nat_cong_sym: "[(a::nat) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
+  by (unfold cong_nat_def, auto)
+
+lemma int_cong_sym: "[(a::int) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
+  by (unfold cong_int_def, auto)
+
+lemma nat_cong_sym_eq: "[(a::nat) = b] (mod m) = [b = a] (mod m)"
+  by (unfold cong_nat_def, auto)
+
+lemma int_cong_sym_eq: "[(a::int) = b] (mod m) = [b = a] (mod m)"
+  by (unfold cong_int_def, auto)
+
+lemma nat_cong_trans [trans]:
+    "[(a::nat) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
+  by (unfold cong_nat_def, auto)
+
+lemma int_cong_trans [trans]:
+    "[(a::int) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
+  by (unfold cong_int_def, auto)
+
+lemma nat_cong_add:
+    "[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
+  apply (unfold cong_nat_def)
+  apply (subst (1 2) mod_add_eq)
+  apply simp
+done
+
+lemma int_cong_add:
+    "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
+  apply (unfold cong_int_def)
+  apply (subst (1 2) mod_add_left_eq)
+  apply (subst (1 2) mod_add_right_eq)
+  apply simp
+done
+
+lemma int_cong_diff:
+    "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a - c = b - d] (mod m)"
+  apply (unfold cong_int_def)
+  apply (subst (1 2) mod_diff_eq)
+  apply simp
+done
+
+lemma int_cong_diff_aux:
+  "(a::int) >= c \<Longrightarrow> b >= d \<Longrightarrow> [(a::int) = b] (mod m) \<Longrightarrow> 
+      [c = d] (mod m) \<Longrightarrow> [tsub a c = tsub b d] (mod m)"
+  apply (subst (1 2) tsub_eq)
+  apply (auto intro: int_cong_diff)
+done;
+
+lemma nat_cong_diff:
+  assumes "(a::nat) >= c" and "b >= d" and "[a = b] (mod m)" and
+    "[c = d] (mod m)"
+  shows "[a - c = b - d] (mod m)"
+
+  using prems by (rule int_cong_diff_aux [transferred]);
+
+lemma nat_cong_mult:
+    "[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
+  apply (unfold cong_nat_def)
+  apply (subst (1 2) mod_mult_eq)
+  apply simp
+done
+
+lemma int_cong_mult:
+    "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
+  apply (unfold cong_int_def)
+  apply (subst (1 2) zmod_zmult1_eq)
+  apply (subst (1 2) mult_commute)
+  apply (subst (1 2) zmod_zmult1_eq)
+  apply simp
+done
+
+lemma nat_cong_exp: "[(x::nat) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
+  apply (induct k)
+  apply (auto simp add: nat_cong_refl nat_cong_mult)
+done
+
+lemma int_cong_exp: "[(x::int) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
+  apply (induct k)
+  apply (auto simp add: int_cong_refl int_cong_mult)
+done
+
+lemma nat_cong_setsum [rule_format]: 
+    "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow> 
+      [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
+  apply (case_tac "finite A")
+  apply (induct set: finite)
+  apply (auto intro: nat_cong_add)
+done
+
+lemma int_cong_setsum [rule_format]:
+    "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow> 
+      [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
+  apply (case_tac "finite A")
+  apply (induct set: finite)
+  apply (auto intro: int_cong_add)
+done
+
+lemma nat_cong_setprod [rule_format]: 
+    "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow> 
+      [(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
+  apply (case_tac "finite A")
+  apply (induct set: finite)
+  apply (auto intro: nat_cong_mult)
+done
+
+lemma int_cong_setprod [rule_format]: 
+    "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow> 
+      [(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
+  apply (case_tac "finite A")
+  apply (induct set: finite)
+  apply (auto intro: int_cong_mult)
+done
+
+lemma nat_cong_scalar: "[(a::nat)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
+  by (rule nat_cong_mult, simp_all)
+
+lemma int_cong_scalar: "[(a::int)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
+  by (rule int_cong_mult, simp_all)
+
+lemma nat_cong_scalar2: "[(a::nat)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
+  by (rule nat_cong_mult, simp_all)
+
+lemma int_cong_scalar2: "[(a::int)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
+  by (rule int_cong_mult, simp_all)
+
+lemma nat_cong_mult_self: "[(a::nat) * m = 0] (mod m)"
+  by (unfold cong_nat_def, auto)
+
+lemma int_cong_mult_self: "[(a::int) * m = 0] (mod m)"
+  by (unfold cong_int_def, auto)
+
+lemma int_cong_eq_diff_cong_0: "[(a::int) = b] (mod m) = [a - b = 0] (mod m)"
+  apply (rule iffI)
+  apply (erule int_cong_diff [of a b m b b, simplified])
+  apply (erule int_cong_add [of "a - b" 0 m b b, simplified])
+done
+
+lemma int_cong_eq_diff_cong_0_aux: "a >= b \<Longrightarrow>
+    [(a::int) = b] (mod m) = [tsub a b = 0] (mod m)"
+  by (subst tsub_eq, assumption, rule int_cong_eq_diff_cong_0)
+
+lemma nat_cong_eq_diff_cong_0:
+  assumes "(a::nat) >= b"
+  shows "[a = b] (mod m) = [a - b = 0] (mod m)"
+
+  using prems by (rule int_cong_eq_diff_cong_0_aux [transferred])
+
+lemma nat_cong_diff_cong_0': 
+  "[(x::nat) = y] (mod n) \<longleftrightarrow> 
+    (if x <= y then [y - x = 0] (mod n) else [x - y = 0] (mod n))"
+  apply (case_tac "y <= x")
+  apply (frule nat_cong_eq_diff_cong_0 [where m = n])
+  apply auto [1]
+  apply (subgoal_tac "x <= y")
+  apply (frule nat_cong_eq_diff_cong_0 [where m = n])
+  apply (subst nat_cong_sym_eq)
+  apply auto
+done
+
+lemma nat_cong_altdef: "(a::nat) >= b \<Longrightarrow> [a = b] (mod m) = (m dvd (a - b))"
+  apply (subst nat_cong_eq_diff_cong_0, assumption)
+  apply (unfold cong_nat_def)
+  apply (simp add: dvd_eq_mod_eq_0 [symmetric])
+done
+
+lemma int_cong_altdef: "[(a::int) = b] (mod m) = (m dvd (a - b))"
+  apply (subst int_cong_eq_diff_cong_0)
+  apply (unfold cong_int_def)
+  apply (simp add: dvd_eq_mod_eq_0 [symmetric])
+done
+
+lemma int_cong_abs: "[(x::int) = y] (mod abs m) = [x = y] (mod m)"
+  by (simp add: int_cong_altdef)
+
+lemma int_cong_square:
+   "\<lbrakk> prime (p::int); 0 < a; [a * a = 1] (mod p) \<rbrakk>
+    \<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)"
+  apply (simp only: int_cong_altdef)
+  apply (subst int_prime_dvd_mult_eq [symmetric], assumption)
+  (* any way around this? *)
+  apply (subgoal_tac "a * a - 1 = (a - 1) * (a - -1)")
+  apply (auto simp add: ring_simps)
+done
+
+lemma int_cong_mult_rcancel:
+  "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
+  apply (subst (1 2) int_cong_altdef)
+  apply (subst left_diff_distrib [symmetric])
+  apply (rule int_coprime_dvd_mult_iff)
+  apply (subst int_gcd_commute, assumption)
+done
+
+lemma nat_cong_mult_rcancel:
+  assumes  "coprime k (m::nat)"
+  shows "[a * k = b * k] (mod m) = [a = b] (mod m)"
+
+  apply (rule int_cong_mult_rcancel [transferred])
+  using prems apply auto
+done
+
+lemma nat_cong_mult_lcancel:
+  "coprime k (m::nat) \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)"
+  by (simp add: mult_commute nat_cong_mult_rcancel)
+
+lemma int_cong_mult_lcancel:
+  "coprime k (m::int) \<Longrightarrow> [k * a = k * b] (mod m) = [a = b] (mod m)"
+  by (simp add: mult_commute int_cong_mult_rcancel)
+
+(* was zcong_zgcd_zmult_zmod *)
+lemma int_coprime_cong_mult:
+  "[(a::int) = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n
+    \<Longrightarrow> [a = b] (mod m * n)"
+  apply (simp only: int_cong_altdef)
+  apply (erule (2) int_divides_mult)
+done
+
+lemma nat_coprime_cong_mult:
+  assumes "[(a::nat) = b] (mod m)" and "[a = b] (mod n)" and "coprime m n"
+  shows "[a = b] (mod m * n)"
+
+  apply (rule int_coprime_cong_mult [transferred])
+  using prems apply auto
+done
+
+lemma nat_cong_less_imp_eq: "0 \<le> (a::nat) \<Longrightarrow>
+    a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b"
+  by (auto simp add: cong_nat_def mod_pos_pos_trivial)
+
+lemma int_cong_less_imp_eq: "0 \<le> (a::int) \<Longrightarrow>
+    a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b"
+  by (auto simp add: cong_int_def mod_pos_pos_trivial)
+
+lemma nat_cong_less_unique:
+    "0 < (m::nat) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
+  apply auto
+  apply (rule_tac x = "a mod m" in exI)
+  apply (unfold cong_nat_def, auto)
+done
+
+lemma int_cong_less_unique:
+    "0 < (m::int) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
+  apply auto
+  apply (rule_tac x = "a mod m" in exI)
+  apply (unfold cong_int_def, auto simp add: mod_pos_pos_trivial)
+done
+
+lemma int_cong_iff_lin: "([(a::int) = b] (mod m)) = (\<exists>k. b = a + m * k)"
+  apply (auto simp add: int_cong_altdef dvd_def ring_simps)
+  apply (rule_tac [!] x = "-k" in exI, auto)
+done
+
+lemma nat_cong_iff_lin: "([(a::nat) = b] (mod m)) = 
+    (\<exists>k1 k2. b + k1 * m = a + k2 * m)"
+  apply (rule iffI)
+  apply (case_tac "b <= a")
+  apply (subst (asm) nat_cong_altdef, assumption)
+  apply (unfold dvd_def, auto)
+  apply (rule_tac x = k in exI)
+  apply (rule_tac x = 0 in exI)
+  apply (auto simp add: ring_simps)
+  apply (subst (asm) nat_cong_sym_eq)
+  apply (subst (asm) nat_cong_altdef)
+  apply force
+  apply (unfold dvd_def, auto)
+  apply (rule_tac x = 0 in exI)
+  apply (rule_tac x = k in exI)
+  apply (auto simp add: ring_simps)
+  apply (unfold cong_nat_def)
+  apply (subgoal_tac "a mod m = (a + k2 * m) mod m")
+  apply (erule ssubst)back
+  apply (erule subst)
+  apply auto
+done
+
+lemma int_cong_gcd_eq: "[(a::int) = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
+  apply (subst (asm) int_cong_iff_lin, auto)
+  apply (subst add_commute) 
+  apply (subst (2) int_gcd_commute)
+  apply (subst mult_commute)
+  apply (subst int_gcd_add_mult)
+  apply (rule int_gcd_commute)
+done
+
+lemma nat_cong_gcd_eq: 
+  assumes "[(a::nat) = b] (mod m)"
+  shows "gcd a m = gcd b m"
+
+  apply (rule int_cong_gcd_eq [transferred])
+  using prems apply auto
+done
+
+lemma nat_cong_imp_coprime: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> 
+    coprime b m"
+  by (auto simp add: nat_cong_gcd_eq)
+
+lemma int_cong_imp_coprime: "[(a::int) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> 
+    coprime b m"
+  by (auto simp add: int_cong_gcd_eq)
+
+lemma nat_cong_cong_mod: "[(a::nat) = b] (mod m) = 
+    [a mod m = b mod m] (mod m)"
+  by (auto simp add: cong_nat_def)
+
+lemma int_cong_cong_mod: "[(a::int) = b] (mod m) = 
+    [a mod m = b mod m] (mod m)"
+  by (auto simp add: cong_int_def)
+
+lemma int_cong_minus [iff]: "[(a::int) = b] (mod -m) = [a = b] (mod m)"
+  by (subst (1 2) int_cong_altdef, auto)
+
+lemma nat_cong_zero [iff]: "[(a::nat) = b] (mod 0) = (a = b)"
+  by (auto simp add: cong_nat_def)
+
+lemma int_cong_zero [iff]: "[(a::int) = b] (mod 0) = (a = b)"
+  by (auto simp add: cong_int_def)
+
+(*
+lemma int_mod_dvd_mod:
+    "0 < (m::int) \<Longrightarrow> m dvd b \<Longrightarrow> (a mod b mod m) = (a mod m)"
+  apply (unfold dvd_def, auto)
+  apply (rule mod_mod_cancel)
+  apply auto
+done
+
+lemma mod_dvd_mod:
+  assumes "0 < (m::nat)" and "m dvd b"
+  shows "(a mod b mod m) = (a mod m)"
+
+  apply (rule int_mod_dvd_mod [transferred])
+  using prems apply auto
+done
+*)
+
+lemma nat_cong_add_lcancel: 
+    "[(a::nat) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)" 
+  by (simp add: nat_cong_iff_lin)
+
+lemma int_cong_add_lcancel: 
+    "[(a::int) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)" 
+  by (simp add: int_cong_iff_lin)
+
+lemma nat_cong_add_rcancel: "[(x::nat) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
+  by (simp add: nat_cong_iff_lin)
+
+lemma int_cong_add_rcancel: "[(x::int) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
+  by (simp add: int_cong_iff_lin)
+
+lemma nat_cong_add_lcancel_0: "[(a::nat) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 
+  by (simp add: nat_cong_iff_lin)
+
+lemma int_cong_add_lcancel_0: "[(a::int) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 
+  by (simp add: int_cong_iff_lin)
+
+lemma nat_cong_add_rcancel_0: "[x + (a::nat) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 
+  by (simp add: nat_cong_iff_lin)
+
+lemma int_cong_add_rcancel_0: "[x + (a::int) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 
+  by (simp add: int_cong_iff_lin)
+
+lemma nat_cong_dvd_modulus: "[(x::nat) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> 
+    [x = y] (mod n)"
+  apply (auto simp add: nat_cong_iff_lin dvd_def)
+  apply (rule_tac x="k1 * k" in exI)
+  apply (rule_tac x="k2 * k" in exI)
+  apply (simp add: ring_simps)
+done
+
+lemma int_cong_dvd_modulus: "[(x::int) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> 
+    [x = y] (mod n)"
+  by (auto simp add: int_cong_altdef dvd_def)
+
+lemma nat_cong_dvd_eq: "[(x::nat) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
+  by (unfold cong_nat_def, auto simp add: dvd_eq_mod_eq_0)
+
+lemma int_cong_dvd_eq: "[(x::int) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
+  by (unfold cong_int_def, auto simp add: dvd_eq_mod_eq_0)
+
+lemma nat_cong_mod: "(n::nat) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)" 
+  by (simp add: cong_nat_def)
+
+lemma int_cong_mod: "(n::int) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)" 
+  by (simp add: cong_int_def)
+
+lemma nat_mod_mult_cong: "(a::nat) ~= 0 \<Longrightarrow> b ~= 0 
+    \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
+  by (simp add: cong_nat_def mod_mult2_eq  mod_add_left_eq)
+
+lemma int_neg_cong: "([(a::int) = b] (mod m)) = ([-a = -b] (mod m))"
+  apply (simp add: int_cong_altdef)
+  apply (subst dvd_minus_iff [symmetric])
+  apply (simp add: ring_simps)
+done
+
+lemma int_cong_modulus_neg: "([(a::int) = b] (mod m)) = ([a = b] (mod -m))"
+  by (auto simp add: int_cong_altdef)
+
+lemma int_mod_mult_cong: "(a::int) ~= 0 \<Longrightarrow> b ~= 0 
+    \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
+  apply (case_tac "b > 0")
+  apply (simp add: cong_int_def mod_mod_cancel mod_add_left_eq)
+  apply (subst (1 2) int_cong_modulus_neg)
+  apply (unfold cong_int_def)
+  apply (subgoal_tac "a * b = (-a * -b)")
+  apply (erule ssubst)
+  apply (subst zmod_zmult2_eq)
+  apply (auto simp add: mod_add_left_eq) 
+done
+
+lemma nat_cong_to_1: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a - 1))"
+  apply (case_tac "a = 0")
+  apply force
+  apply (subst (asm) nat_cong_altdef)
+  apply auto
+done
+
+lemma nat_0_cong_1: "[(0::nat) = 1] (mod n) = (n = 1)"
+  by (unfold cong_nat_def, auto)
+
+lemma int_0_cong_1: "[(0::int) = 1] (mod n) = ((n = 1) | (n = -1))"
+  by (unfold cong_int_def, auto simp add: zmult_eq_1_iff)
+
+lemma nat_cong_to_1': "[(a::nat) = 1] (mod n) \<longleftrightarrow> 
+    a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)"
+  apply (case_tac "n = 1")
+  apply auto [1]
+  apply (drule_tac x = "a - 1" in spec)
+  apply force
+  apply (case_tac "a = 0")
+  apply (auto simp add: nat_0_cong_1) [1]
+  apply (rule iffI)
+  apply (drule nat_cong_to_1)
+  apply (unfold dvd_def)
+  apply auto [1]
+  apply (rule_tac x = k in exI)
+  apply (auto simp add: ring_simps) [1]
+  apply (subst nat_cong_altdef)
+  apply (auto simp add: dvd_def)
+done
+
+lemma nat_cong_le: "(y::nat) <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
+  apply (subst nat_cong_altdef)
+  apply assumption
+  apply (unfold dvd_def, auto simp add: ring_simps)
+  apply (rule_tac x = k in exI)
+  apply auto
+done
+
+lemma nat_cong_solve: "(a::nat) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
+  apply (case_tac "n = 0")
+  apply force
+  apply (frule nat_bezout [of a n], auto)
+  apply (rule exI, erule ssubst)
+  apply (rule nat_cong_trans)
+  apply (rule nat_cong_add)
+  apply (subst mult_commute)
+  apply (rule nat_cong_mult_self)
+  prefer 2
+  apply simp
+  apply (rule nat_cong_refl)
+  apply (rule nat_cong_refl)
+done
+
+lemma int_cong_solve: "(a::int) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
+  apply (case_tac "n = 0")
+  apply (case_tac "a \<ge> 0")
+  apply auto
+  apply (rule_tac x = "-1" in exI)
+  apply auto
+  apply (insert int_bezout [of a n], auto)
+  apply (rule exI)
+  apply (erule subst)
+  apply (rule int_cong_trans)
+  prefer 2
+  apply (rule int_cong_add)
+  apply (rule int_cong_refl)
+  apply (rule int_cong_sym)
+  apply (rule int_cong_mult_self)
+  apply simp
+  apply (subst mult_commute)
+  apply (rule int_cong_refl)
+done
+  
+lemma nat_cong_solve_dvd: 
+  assumes a: "(a::nat) \<noteq> 0" and b: "gcd a n dvd d"
+  shows "EX x. [a * x = d] (mod n)"
+proof -
+  from nat_cong_solve [OF a] obtain x where 
+      "[a * x = gcd a n](mod n)"
+    by auto
+  hence "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)" 
+    by (elim nat_cong_scalar2)
+  also from b have "(d div gcd a n) * gcd a n = d"
+    by (rule dvd_div_mult_self)
+  also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)"
+    by auto
+  finally show ?thesis
+    by auto
+qed
+
+lemma int_cong_solve_dvd: 
+  assumes a: "(a::int) \<noteq> 0" and b: "gcd a n dvd d"
+  shows "EX x. [a * x = d] (mod n)"
+proof -
+  from int_cong_solve [OF a] obtain x where 
+      "[a * x = gcd a n](mod n)"
+    by auto
+  hence "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)" 
+    by (elim int_cong_scalar2)
+  also from b have "(d div gcd a n) * gcd a n = d"
+    by (rule dvd_div_mult_self)
+  also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)"
+    by auto
+  finally show ?thesis
+    by auto
+qed
+
+lemma nat_cong_solve_coprime: "coprime (a::nat) n \<Longrightarrow> 
+    EX x. [a * x = 1] (mod n)"
+  apply (case_tac "a = 0")
+  apply force
+  apply (frule nat_cong_solve [of a n])
+  apply auto
+done
+
+lemma int_cong_solve_coprime: "coprime (a::int) n \<Longrightarrow> 
+    EX x. [a * x = 1] (mod n)"
+  apply (case_tac "a = 0")
+  apply auto
+  apply (case_tac "n \<ge> 0")
+  apply auto
+  apply (subst cong_int_def, auto)
+  apply (frule int_cong_solve [of a n])
+  apply auto
+done
+
+lemma nat_coprime_iff_invertible: "m > (1::nat) \<Longrightarrow> coprime a m = 
+    (EX x. [a * x = 1] (mod m))"
+  apply (auto intro: nat_cong_solve_coprime)
+  apply (unfold cong_nat_def, auto intro: nat_invertible_coprime)
+done
+
+lemma int_coprime_iff_invertible: "m > (1::int) \<Longrightarrow> coprime a m = 
+    (EX x. [a * x = 1] (mod m))"
+  apply (auto intro: int_cong_solve_coprime)
+  apply (unfold cong_int_def)
+  apply (auto intro: int_invertible_coprime)
+done
+
+lemma int_coprime_iff_invertible': "m > (1::int) \<Longrightarrow> coprime a m = 
+    (EX x. 0 <= x & x < m & [a * x = 1] (mod m))"
+  apply (subst int_coprime_iff_invertible)
+  apply auto
+  apply (auto simp add: cong_int_def)
+  apply (rule_tac x = "x mod m" in exI)
+  apply (auto simp add: mod_mult_right_eq [symmetric])
+done
+
+
+lemma nat_cong_cong_lcm: "[(x::nat) = y] (mod a) \<Longrightarrow>
+    [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
+  apply (case_tac "y \<le> x")
+  apply (auto simp add: nat_cong_altdef nat_lcm_least) [1]
+  apply (rule nat_cong_sym)
+  apply (subst (asm) (1 2) nat_cong_sym_eq)
+  apply (auto simp add: nat_cong_altdef nat_lcm_least)
+done
+
+lemma int_cong_cong_lcm: "[(x::int) = y] (mod a) \<Longrightarrow>
+    [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
+  by (auto simp add: int_cong_altdef int_lcm_least) [1]
+
+lemma nat_cong_cong_coprime: "coprime a b \<Longrightarrow> [(x::nat) = y] (mod a) \<Longrightarrow>
+    [x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
+  apply (frule (1) nat_cong_cong_lcm)back
+  apply (simp add: lcm_nat_def)
+done
+
+lemma int_cong_cong_coprime: "coprime a b \<Longrightarrow> [(x::int) = y] (mod a) \<Longrightarrow>
+    [x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
+  apply (frule (1) int_cong_cong_lcm)back
+  apply (simp add: int_lcm_altdef int_cong_abs abs_mult [symmetric])
+done
+
+lemma nat_cong_cong_setprod_coprime [rule_format]: "finite A \<Longrightarrow>
+    (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
+    (ALL i:A. [(x::nat) = y] (mod m i)) \<longrightarrow>
+      [x = y] (mod (PROD i:A. m i))"
+  apply (induct set: finite)
+  apply auto
+  apply (rule nat_cong_cong_coprime)
+  apply (subst nat_gcd_commute)
+  apply (rule nat_setprod_coprime)
+  apply auto
+done
+
+lemma int_cong_cong_setprod_coprime [rule_format]: "finite A \<Longrightarrow>
+    (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
+    (ALL i:A. [(x::int) = y] (mod m i)) \<longrightarrow>
+      [x = y] (mod (PROD i:A. m i))"
+  apply (induct set: finite)
+  apply auto
+  apply (rule int_cong_cong_coprime)
+  apply (subst int_gcd_commute)
+  apply (rule int_setprod_coprime)
+  apply auto
+done
+
+lemma nat_binary_chinese_remainder_aux: 
+  assumes a: "coprime (m1::nat) m2"
+  shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
+    [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
+proof -
+  from nat_cong_solve_coprime [OF a]
+      obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
+    by auto
+  from a have b: "coprime m2 m1" 
+    by (subst nat_gcd_commute)
+  from nat_cong_solve_coprime [OF b]
+      obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
+    by auto
+  have "[m1 * x1 = 0] (mod m1)"
+    by (subst mult_commute, rule nat_cong_mult_self)
+  moreover have "[m2 * x2 = 0] (mod m2)"
+    by (subst mult_commute, rule nat_cong_mult_self)
+  moreover note one two
+  ultimately show ?thesis by blast
+qed
+
+lemma int_binary_chinese_remainder_aux: 
+  assumes a: "coprime (m1::int) m2"
+  shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
+    [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
+proof -
+  from int_cong_solve_coprime [OF a]
+      obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
+    by auto
+  from a have b: "coprime m2 m1" 
+    by (subst int_gcd_commute)
+  from int_cong_solve_coprime [OF b]
+      obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
+    by auto
+  have "[m1 * x1 = 0] (mod m1)"
+    by (subst mult_commute, rule int_cong_mult_self)
+  moreover have "[m2 * x2 = 0] (mod m2)"
+    by (subst mult_commute, rule int_cong_mult_self)
+  moreover note one two
+  ultimately show ?thesis by blast
+qed
+
+lemma nat_binary_chinese_remainder:
+  assumes a: "coprime (m1::nat) m2"
+  shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
+proof -
+  from nat_binary_chinese_remainder_aux [OF a] obtain b1 b2
+    where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
+          "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
+    by blast
+  let ?x = "u1 * b1 + u2 * b2"
+  have "[?x = u1 * 1 + u2 * 0] (mod m1)"
+    apply (rule nat_cong_add)
+    apply (rule nat_cong_scalar2)
+    apply (rule `[b1 = 1] (mod m1)`)
+    apply (rule nat_cong_scalar2)
+    apply (rule `[b2 = 0] (mod m1)`)
+    done
+  hence "[?x = u1] (mod m1)" by simp
+  have "[?x = u1 * 0 + u2 * 1] (mod m2)"
+    apply (rule nat_cong_add)
+    apply (rule nat_cong_scalar2)
+    apply (rule `[b1 = 0] (mod m2)`)
+    apply (rule nat_cong_scalar2)
+    apply (rule `[b2 = 1] (mod m2)`)
+    done
+  hence "[?x = u2] (mod m2)" by simp
+  with `[?x = u1] (mod m1)` show ?thesis by blast
+qed
+
+lemma int_binary_chinese_remainder:
+  assumes a: "coprime (m1::int) m2"
+  shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
+proof -
+  from int_binary_chinese_remainder_aux [OF a] obtain b1 b2
+    where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
+          "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
+    by blast
+  let ?x = "u1 * b1 + u2 * b2"
+  have "[?x = u1 * 1 + u2 * 0] (mod m1)"
+    apply (rule int_cong_add)
+    apply (rule int_cong_scalar2)
+    apply (rule `[b1 = 1] (mod m1)`)
+    apply (rule int_cong_scalar2)
+    apply (rule `[b2 = 0] (mod m1)`)
+    done
+  hence "[?x = u1] (mod m1)" by simp
+  have "[?x = u1 * 0 + u2 * 1] (mod m2)"
+    apply (rule int_cong_add)
+    apply (rule int_cong_scalar2)
+    apply (rule `[b1 = 0] (mod m2)`)
+    apply (rule int_cong_scalar2)
+    apply (rule `[b2 = 1] (mod m2)`)
+    done
+  hence "[?x = u2] (mod m2)" by simp
+  with `[?x = u1] (mod m1)` show ?thesis by blast
+qed
+
+lemma nat_cong_modulus_mult: "[(x::nat) = y] (mod m * n) \<Longrightarrow> 
+    [x = y] (mod m)"
+  apply (case_tac "y \<le> x")
+  apply (simp add: nat_cong_altdef)
+  apply (erule dvd_mult_left)
+  apply (rule nat_cong_sym)
+  apply (subst (asm) nat_cong_sym_eq)
+  apply (simp add: nat_cong_altdef) 
+  apply (erule dvd_mult_left)
+done
+
+lemma int_cong_modulus_mult: "[(x::int) = y] (mod m * n) \<Longrightarrow> 
+    [x = y] (mod m)"
+  apply (simp add: int_cong_altdef) 
+  apply (erule dvd_mult_left)
+done
+
+lemma nat_cong_less_modulus_unique: 
+    "[(x::nat) = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y"
+  by (simp add: cong_nat_def)
+
+lemma nat_binary_chinese_remainder_unique:
+  assumes a: "coprime (m1::nat) m2" and
+         nz: "m1 \<noteq> 0" "m2 \<noteq> 0"
+  shows "EX! x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
+proof -
+  from nat_binary_chinese_remainder [OF a] obtain y where 
+      "[y = u1] (mod m1)" and "[y = u2] (mod m2)"
+    by blast
+  let ?x = "y mod (m1 * m2)"
+  from nz have less: "?x < m1 * m2"
+    by auto   
+  have one: "[?x = u1] (mod m1)"
+    apply (rule nat_cong_trans)
+    prefer 2
+    apply (rule `[y = u1] (mod m1)`)
+    apply (rule nat_cong_modulus_mult)
+    apply (rule nat_cong_mod)
+    using nz apply auto
+    done
+  have two: "[?x = u2] (mod m2)"
+    apply (rule nat_cong_trans)
+    prefer 2
+    apply (rule `[y = u2] (mod m2)`)
+    apply (subst mult_commute)
+    apply (rule nat_cong_modulus_mult)
+    apply (rule nat_cong_mod)
+    using nz apply auto
+    done
+  have "ALL z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow>
+      z = ?x"
+  proof (clarify)
+    fix z
+    assume "z < m1 * m2"
+    assume "[z = u1] (mod m1)" and  "[z = u2] (mod m2)"
+    have "[?x = z] (mod m1)"
+      apply (rule nat_cong_trans)
+      apply (rule `[?x = u1] (mod m1)`)
+      apply (rule nat_cong_sym)
+      apply (rule `[z = u1] (mod m1)`)
+      done
+    moreover have "[?x = z] (mod m2)"
+      apply (rule nat_cong_trans)
+      apply (rule `[?x = u2] (mod m2)`)
+      apply (rule nat_cong_sym)
+      apply (rule `[z = u2] (mod m2)`)
+      done
+    ultimately have "[?x = z] (mod m1 * m2)"
+      by (auto intro: nat_coprime_cong_mult a)
+    with `z < m1 * m2` `?x < m1 * m2` show "z = ?x"
+      apply (intro nat_cong_less_modulus_unique)
+      apply (auto, erule nat_cong_sym)
+      done
+  qed  
+  with less one two show ?thesis
+    by auto
+ qed
+
+lemma nat_chinese_remainder_aux:
+  fixes A :: "'a set" and
+        m :: "'a \<Rightarrow> nat"
+  assumes fin: "finite A" and
+          cop: "ALL i : A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
+  shows "EX b. (ALL i : A. 
+      [b i = 1] (mod m i) \<and> [b i = 0] (mod (PROD j : A - {i}. m j)))"
+proof (rule finite_set_choice, rule fin, rule ballI)
+  fix i
+  assume "i : A"
+  with cop have "coprime (PROD j : A - {i}. m j) (m i)"
+    by (intro nat_setprod_coprime, auto)
+  hence "EX x. [(PROD j : A - {i}. m j) * x = 1] (mod m i)"
+    by (elim nat_cong_solve_coprime)
+  then obtain x where "[(PROD j : A - {i}. m j) * x = 1] (mod m i)"
+    by auto
+  moreover have "[(PROD j : A - {i}. m j) * x = 0] 
+    (mod (PROD j : A - {i}. m j))"
+    by (subst mult_commute, rule nat_cong_mult_self)
+  ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0] 
+      (mod setprod m (A - {i}))"
+    by blast
+qed
+
+lemma nat_chinese_remainder:
+  fixes A :: "'a set" and
+        m :: "'a \<Rightarrow> nat" and
+        u :: "'a \<Rightarrow> nat"
+  assumes 
+        fin: "finite A" and
+        cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
+  shows "EX x. (ALL i:A. [x = u i] (mod m i))"
+proof -
+  from nat_chinese_remainder_aux [OF fin cop] obtain b where
+    bprop: "ALL i:A. [b i = 1] (mod m i) \<and> 
+      [b i = 0] (mod (PROD j : A - {i}. m j))"
+    by blast
+  let ?x = "SUM i:A. (u i) * (b i)"
+  show "?thesis"
+  proof (rule exI, clarify)
+    fix i
+    assume a: "i : A"
+    show "[?x = u i] (mod m i)" 
+    proof -
+      from fin a have "?x = (SUM j:{i}. u j * b j) + 
+          (SUM j:A-{i}. u j * b j)"
+        by (subst setsum_Un_disjoint [symmetric], auto intro: setsum_cong)
+      hence "[?x = u i * b i + (SUM j:A-{i}. u j * b j)] (mod m i)"
+        by auto
+      also have "[u i * b i + (SUM j:A-{i}. u j * b j) =
+                  u i * 1 + (SUM j:A-{i}. u j * 0)] (mod m i)"
+        apply (rule nat_cong_add)
+        apply (rule nat_cong_scalar2)
+        using bprop a apply blast
+        apply (rule nat_cong_setsum)
+        apply (rule nat_cong_scalar2)
+        using bprop apply auto
+        apply (rule nat_cong_dvd_modulus)
+        apply (drule (1) bspec)
+        apply (erule conjE)
+        apply assumption
+        apply (rule dvd_setprod)
+        using fin a apply auto
+        done
+      finally show ?thesis
+        by simp
+    qed
+  qed
+qed
+
+lemma nat_coprime_cong_prod [rule_format]: "finite A \<Longrightarrow> 
+    (ALL i: A. (ALL j: A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
+      (ALL i: A. [(x::nat) = y] (mod m i)) \<longrightarrow>
+         [x = y] (mod (PROD i:A. m i))" 
+  apply (induct set: finite)
+  apply auto
+  apply (erule (1) nat_coprime_cong_mult)
+  apply (subst nat_gcd_commute)
+  apply (rule nat_setprod_coprime)
+  apply auto
+done
+
+lemma nat_chinese_remainder_unique:
+  fixes A :: "'a set" and
+        m :: "'a \<Rightarrow> nat" and
+        u :: "'a \<Rightarrow> nat"
+  assumes 
+        fin: "finite A" and
+         nz: "ALL i:A. m i \<noteq> 0" and
+        cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
+  shows "EX! x. x < (PROD i:A. m i) \<and> (ALL i:A. [x = u i] (mod m i))"
+proof -
+  from nat_chinese_remainder [OF fin cop] obtain y where
+      one: "(ALL i:A. [y = u i] (mod m i))" 
+    by blast
+  let ?x = "y mod (PROD i:A. m i)"
+  from fin nz have prodnz: "(PROD i:A. m i) \<noteq> 0"
+    by auto
+  hence less: "?x < (PROD i:A. m i)"
+    by auto
+  have cong: "ALL i:A. [?x = u i] (mod m i)"
+    apply auto
+    apply (rule nat_cong_trans)
+    prefer 2
+    using one apply auto
+    apply (rule nat_cong_dvd_modulus)
+    apply (rule nat_cong_mod)
+    using prodnz apply auto
+    apply (rule dvd_setprod)
+    apply (rule fin)
+    apply assumption
+    done
+  have unique: "ALL z. z < (PROD i:A. m i) \<and> 
+      (ALL i:A. [z = u i] (mod m i)) \<longrightarrow> z = ?x"
+  proof (clarify)
+    fix z
+    assume zless: "z < (PROD i:A. m i)"
+    assume zcong: "(ALL i:A. [z = u i] (mod m i))"
+    have "ALL i:A. [?x = z] (mod m i)"
+      apply clarify     
+      apply (rule nat_cong_trans)
+      using cong apply (erule bspec)
+      apply (rule nat_cong_sym)
+      using zcong apply auto
+      done
+    with fin cop have "[?x = z] (mod (PROD i:A. m i))"
+      by (intro nat_coprime_cong_prod, auto)
+    with zless less show "z = ?x"
+      apply (intro nat_cong_less_modulus_unique)
+      apply (auto, erule nat_cong_sym)
+      done
+  qed 
+  from less cong unique show ?thesis
+    by blast  
+qed
+
+end