--- 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>
--- 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])
--- 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