# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1640516487 0
# Node ID 9469d922368930243378b4337a59138110def174
# Parent  77a96ed74340d5685ecab27ead848b4e959b5398
Tiny additions inspired by Roth development

diff -r 77a96ed74340 -r 9469d9223689 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Tue Dec 21 22:11:10 2021 +0100
+++ b/src/HOL/GCD.thy	Sun Dec 26 11:01:27 2021 +0000
@@ -1637,6 +1637,26 @@
 
 end
 
+text \<open>And some consequences: cancellation modulo @{term m}\<close>
+lemma mult_mod_cancel_right:
+  fixes m :: "'a::{euclidean_ring_cancel,semiring_gcd}"
+  assumes eq: "(a * n) mod m = (b * n) mod m" and "coprime m n" 
+  shows "a mod m = b mod m"
+proof -
+  have "m dvd (a*n - b*n)" 
+    using eq mod_eq_dvd_iff by blast
+  then have "m dvd a-b"
+    by (metis \<open>coprime m n\<close> coprime_dvd_mult_left_iff left_diff_distrib')
+  then show ?thesis
+    using mod_eq_dvd_iff by blast
+qed
+
+lemma mult_mod_cancel_left:
+  fixes m :: "'a::{euclidean_ring_cancel,semiring_gcd}"
+  assumes "(n * a) mod m = (n * b) mod m" and "coprime m n" 
+  shows "a mod m = b mod m"
+  by (metis assms mult.commute mult_mod_cancel_right)
+
 
 subsection \<open>GCD and LCM for multiplicative normalisation functions\<close>
 
diff -r 77a96ed74340 -r 9469d9223689 src/HOL/Library/Nat_Bijection.thy
--- a/src/HOL/Library/Nat_Bijection.thy	Tue Dec 21 22:11:10 2021 +0100
+++ b/src/HOL/Library/Nat_Bijection.thy	Sun Dec 26 11:01:27 2021 +0000
@@ -87,10 +87,10 @@
 lemma bij_prod_decode: "bij prod_decode"
   by (rule bijI [OF inj_prod_decode surj_prod_decode])
 
-lemma prod_encode_eq: "prod_encode x = prod_encode y \<longleftrightarrow> x = y"
+lemma prod_encode_eq [simp]: "prod_encode x = prod_encode y \<longleftrightarrow> x = y"
   by (rule inj_prod_encode [THEN inj_eq])
 
-lemma prod_decode_eq: "prod_decode x = prod_decode y \<longleftrightarrow> x = y"
+lemma prod_decode_eq [simp]: "prod_decode x = prod_decode y \<longleftrightarrow> x = y"
   by (rule inj_prod_decode [THEN inj_eq])
 
 
diff -r 77a96ed74340 -r 9469d9223689 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Tue Dec 21 22:11:10 2021 +0100
+++ b/src/HOL/Set_Interval.thy	Sun Dec 26 11:01:27 2021 +0000
@@ -22,6 +22,9 @@
 lemma card_2_iff': "card S = 2 \<longleftrightarrow> (\<exists>x\<in>S. \<exists>y\<in>S. x \<noteq> y \<and> (\<forall>z\<in>S. z = x \<or> z = y))"
   by (auto simp: card_Suc_eq numeral_eq_Suc)
 
+lemma card_3_iff: "card S = 3 \<longleftrightarrow> (\<exists>x y z. S = {x,y,z} \<and> x \<noteq> y \<and> y \<noteq> z \<and> x \<noteq> z)"
+  by (fastforce simp: card_Suc_eq numeral_eq_Suc)
+
 context ord
 begin