diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Parity.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -318,6 +318,38 @@
   using mult_div_mod_eq [of 2 a]
   by (simp add: even_iff_mod_2_eq_zero)
 
+lemma coprime_left_2_iff_odd [simp]:
+  "coprime 2 a \<longleftrightarrow> odd a"
+proof
+  assume "odd a"
+  show "coprime 2 a"
+  proof (rule coprimeI)
+    fix b
+    assume "b dvd 2" "b dvd a"
+    then have "b dvd a mod 2"
+      by (auto intro: dvd_mod)
+    with \<open>odd a\<close> show "is_unit b"
+      by (simp add: mod_2_eq_odd)
+  qed
+next
+  assume "coprime 2 a"
+  show "odd a"
+  proof (rule notI)
+    assume "even a"
+    then obtain b where "a = 2 * b" ..
+    with \<open>coprime 2 a\<close> have "coprime 2 (2 * b)"
+      by simp
+    moreover have "\<not> coprime 2 (2 * b)"
+      by (rule not_coprimeI [of 2]) simp_all
+    ultimately show False
+      by blast
+  qed
+qed
+
+lemma coprime_right_2_iff_odd [simp]:
+  "coprime a 2 \<longleftrightarrow> odd a"
+  using coprime_left_2_iff_odd [of a] by (simp add: ac_simps)
+
 end
 
 class ring_parity = ring + semiring_parity