diff --git a/thys/Polygonal_Number_Theorem/Polygonal_Number_Theorem_Cauchy.thy b/thys/Polygonal_Number_Theorem/Polygonal_Number_Theorem_Cauchy.thy
--- a/thys/Polygonal_Number_Theorem/Polygonal_Number_Theorem_Cauchy.thy
+++ b/thys/Polygonal_Number_Theorem/Polygonal_Number_Theorem_Cauchy.thy
@@ -1,732 +1,734 @@
 subsection \<open> Cauchy's Polygonal Number Theorem \<close>
 
-text \<open>We will use the definition of the polygonal numbers from the Gauss Theorem theory file 
+text \<open>We will use the definition of the polygonal numbers from the Gauss Theorem theory file
 which also imports the Three Squares Theorem AFP entry \cite{Three_Squares-AFP}.\<close>
 
 theory Polygonal_Number_Theorem_Cauchy
   imports Polygonal_Number_Theorem_Gauss
 begin
 
 text\<open>The following lemma shows there are two consecutive odd integers in any four consecutive
 integers.\<close>
 
 lemma two_consec_odd:
   fixes a1 a2 a3 a4 :: int
   assumes "a1-a2 = 1"
   assumes "a2-a3 = 1"
   assumes "a3-a4 = 1"
   shows "\<exists>k1 k2 :: int. {k1, k2} \<subseteq> {a1, a2, a3, a4} \<and> (k2 = k1+2) \<and> odd k1"
 
 proof -
-  have c1:"\<exists>k1 k2 :: int. {k1, k2} \<subseteq> {a1, a2, a3, a4} \<and> (k2 = k1+2) \<and> odd k1" 
+  have c1:"\<exists>k1 k2 :: int. {k1, k2} \<subseteq> {a1, a2, a3, a4} \<and> (k2 = k1+2) \<and> odd k1"
     if odd_case:"odd a4"
   proof-
     define k1 where k1_def:"k1 = a4"
     define k2 where k2_def:"k2 = k1 + 2"
     have 0:"k2 = a2" using k2_def k1_def assms by simp
     have 1:"odd k1" using k1_def odd_case by simp
-    show "\<exists>k1 k2 :: int. {k1, k2} \<subseteq> {a1, a2, a3, a4} \<and> (k2 = k1+2) \<and> odd k1" 
+    show "\<exists>k1 k2 :: int. {k1, k2} \<subseteq> {a1, a2, a3, a4} \<and> (k2 = k1+2) \<and> odd k1"
       using 0 1 k1_def k2_def by auto
   qed
 
-  have c2:"\<exists>k1 k2 :: int. {k1, k2} \<subseteq> {a1, a2, a3, a4} \<and> (k2 = k1+2) \<and> odd k1" 
+  have c2:"\<exists>k1 k2 :: int. {k1, k2} \<subseteq> {a1, a2, a3, a4} \<and> (k2 = k1+2) \<and> odd k1"
     if even_case:"even a4"
   proof -
     define k1 where k1_def:"k1 = a3"
     define k2 where k2_def:"k2 = k1 + 2"
     have 2:"odd k1" using even_case assms k1_def by presburger
     have 3:"k2 = a1" using k1_def k2_def assms by simp
     show "\<exists>k1 k2 :: int. {k1, k2} \<subseteq> {a1, a2, a3, a4} \<and> (k2 = k1+2) \<and> odd k1"
       using 2 3 k1_def k2_def by auto
   qed
   show ?thesis using c1 c2 by auto
 qed
 
 text \<open>This lemma proves that for two consecutive integers $b_1$ and $b_2$, and $r \in \{0,1,\dots,m-3\}$,
 numbers of the form $b_1+r$ and $b_2+r$ can cover all the congruence classes modulo $m$.\<close>
 
 lemma cong_classes:
   fixes b1 b2 :: int
   fixes m :: nat
   assumes "m \<ge> 4"
   assumes "odd b1"
   assumes "b2 = b1 + 2"
   shows "\<forall>N::nat. \<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)"
 
 proof -
   have first:"\<forall>N::nat. \<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)"
     if first_assum:"b1 mod m \<ge> 3"
   proof -
     define k1 where k1_def:"k1 = b1 mod m"
     define l where l_def:"l = m - k1"
     have k1_size:"k1\<ge>3" using first_assum k1_def by simp
     have l_size:"l \<le> m-3" using first_assum k1_def l_def by auto
     have "(l+k1) mod m = 0" using l_def by auto
     hence "(l+b1) mod m = 0" using k1_def l_def by (metis mod_add_right_eq)
     define w where w_def:"w = m-3-l"
-    have w_size:"w\<ge>0 \<and> w\<le>m-3" using w_def l_size l_def k1_def first_assum 
-      by (smt (verit, best) Euclidean_Division.pos_mod_bound assms(1) le_antisym numeral_neq_zero
+    have w_size:"w\<ge>0 \<and> w\<le>m-3" using w_def l_size l_def k1_def first_assum
+      by (smt (verit, best) Euclidean_Rings.pos_mod_bound assms(1) le_antisym numeral_neq_zero
  of_nat_0_less_iff order_trans_rules(22) verit_comp_simplify(3) zero_le_numeral)
     have "k1 = w+3" using w_def k1_def l_def w_size first_assum by linarith
     hence "w+2 = k1-1" by auto
     hence "w+2 = (b1-1) mod m" using first_assum k1_def
-      by (smt (verit, del_insts) Euclidean_Division.pos_mod_bound assms(1)
+      by (smt (verit, del_insts) Euclidean_Rings.pos_mod_bound assms(1)
  mod_diff_eq mod_pos_pos_trivial of_nat_le_0_iff verit_comp_simplify(8))
     hence w_cover:"w+2 = k1-1" using k1_def using \<open>w + 2 = k1 - 1\<close> by fastforce
 
     have "\<exists>r::nat. (r\<le>m-3) \<and> [N=b1+r] (mod m)" if asm1:"N mod m \<ge> k1 \<and> N mod m \<le> m-1" for N
     proof -
       have "m - (N mod m) \<le> l" using asm1 l_def k1_def by linarith
-      hence "\<exists>d::nat. d\<le>l \<and> [N = k1+d] (mod m)" using asm1 k1_def l_def 
+      hence "\<exists>d::nat. d\<le>l \<and> [N = k1+d] (mod m)" using asm1 k1_def l_def
         by (metis add.commute add_le_cancel_left cong_mod_left cong_refl diff_add_cancel
  diff_le_self le_trans of_nat_mod of_nat_mono zle_iff_zadd)
-      hence "\<exists>d::nat. d\<le>l \<and> [N=b1+d] (mod m)" using  k1_def 
-        by (metis mod_add_left_eq unique_euclidean_semiring_class.cong_def) 
-      thus "\<exists>r::nat. (r\<le>m-3) \<and> [N=b1+r] (mod m)" using l_size 
+      hence "\<exists>d::nat. d\<le>l \<and> [N=b1+d] (mod m)" using  k1_def
+        by (metis mod_add_left_eq unique_euclidean_semiring_class.cong_def)
+      thus "\<exists>r::nat. (r\<le>m-3) \<and> [N=b1+r] (mod m)" using l_size
         by (smt (verit, best) nat_leq_as_int)
     qed
     hence c1:"\<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)" if asm1:"N mod m \<ge> k1 \<and> N mod m \<le> m-1" for N using asm1 by blast
 
-    have c2:"\<exists>r::nat. (r\<le>m-3) \<and> [N=b1+r] (mod m)" if asm2:"N mod m =0" for N using l_def k1_def 
+    have c2:"\<exists>r::nat. (r\<le>m-3) \<and> [N=b1+r] (mod m)" if asm2:"N mod m =0" for N using l_def k1_def
       by (smt (verit, ccfv_threshold) \<open>(l + b1) mod int m = 0\<close> add_diff_cancel_left' cong_0_iff
- cong_sym cong_trans diff_add_cancel diff_ge_0_iff_ge dvd_eq_mod_eq_0 int_dvd_int_iff nat_0_le 
+ cong_sym cong_trans diff_add_cancel diff_ge_0_iff_ge dvd_eq_mod_eq_0 int_dvd_int_iff nat_0_le
 of_nat_le_iff that w_def w_size)
     hence c2:"\<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)"
       if asm2:"N mod m = 0" for N using asm2 by metis
 
     have "\<exists>r::nat. (r\<le>m-3) \<and> [N=b1+r] (mod m)" if asm3:"N mod m > 0 \<and> N mod m \<le>w" for N
     proof -
       have "l+ (N mod m) \<le> m-3" using asm3 w_def by auto
       hence "\<exists>d::nat. (d\<le>w) \<and> [N = k1+l+d] (mod m)" using asm3 w_def k1_def l_def
-        by (smt (verit, ccfv_threshold) minus_mod_self2 mod_mod_trivial of_nat_mod 
+        by (smt (verit, ccfv_threshold) minus_mod_self2 mod_mod_trivial of_nat_mod
             unique_euclidean_semiring_class.cong_def)
       hence "\<exists>d::nat. (d\<le>w) \<and> [N = b1+l+d] (mod m)" using k1_def by (metis (mono_tags,
               opaque_lifting) mod_add_left_eq unique_euclidean_semiring_class.cong_def)
-      hence "\<exists>r::nat. (r\<le>w+l) \<and> [N = b1+r] (mod m)" by (smt (verit) add.commute 
+      hence "\<exists>r::nat. (r\<le>w+l) \<and> [N = b1+r] (mod m)" by (smt (verit) add.commute
             add.left_commute le_add_same_cancel2 of_nat_0_le_iff w_def w_size zero_le_imp_eq_int)
       thus "\<exists>r::nat. (r\<le>m-3) \<and> [N = b1+r] (mod m)" using w_def by auto
     qed
     hence "\<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)"
       if asm3:"N mod m > 0 \<and> N mod m \<le>w" for N using asm3 by blast
     hence c3:"\<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)"
       if asm8:"N mod m > 0 \<and> N mod m \<le>k1-3" using asm8 w_cover by auto
 
     have "\<exists>r::nat. (r\<le>m-3) \<and> [N=b2+r] (mod m)" if asm4:"N mod m = w+1 \<or> N mod m = w+2" for N
     proof -
-      have c4_1:"[N = b2+(m-3)] (mod m)" if asm5:"N mod m=w+2" for N using asm5 w_def assms(3) l_def 
+      have c4_1:"[N = b2+(m-3)] (mod m)" if asm5:"N mod m=w+2" for N using asm5 w_def assms(3) l_def
         by (smt (verit) \<open>w + 2 = (b1 - 1) mod int m\<close> \<open>w + 2 = k1 - 1\<close> mod_add_self1 of_nat_mod
             unique_euclidean_semiring_class.cong_def)
       hence "[N-1 = b2+(m-4)] (mod m)" if asm5:"N mod m = w+2" for N
         by (smt (verit, ccfv_threshold) Num.of_nat_simps(2) \<open>w + 2 = k1 - 1\<close> asm5 assms(1)
- cong_iff_lin first_assum k1_def l_def mod_less_eq_dividend numeral_Bit0 of_nat_diff of_nat_le_iff 
-of_nat_numeral semiring_norm(172) w_def) 
-      hence "[N = b2+(m-4)] (mod m)" if asm6:"N mod m = w+1" for N using asm6  
-        by (metis \<open>w + 2 = (b1 - 1) mod int m\<close> add_diff_cancel_right' arith_special(3) int_ops(4) 
+ cong_iff_lin first_assum k1_def l_def mod_less_eq_dividend numeral_Bit0 of_nat_diff of_nat_le_iff
+of_nat_numeral semiring_norm(172) w_def)
+      hence "[N = b2+(m-4)] (mod m)" if asm6:"N mod m = w+1" for N using asm6
+        by (metis \<open>w + 2 = (b1 - 1) mod int m\<close> add_diff_cancel_right' arith_special(3) int_ops(4)
             is_num_normalize(1) mod_add_left_eq mod_diff_left_eq of_nat_mod)
       thus ?thesis using c4_1 by (metis asm4 diff_le_mono2 nat_le_linear numeral_le_iff
             verit_comp_simplify(10) verit_comp_simplify(13))
     qed
     hence "\<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)"
       if asm4:"N mod m = w+1 \<or> N mod m = w+2" for N using asm4 by blast
-    hence c4:"\<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)" 
+    hence c4:"\<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)"
       if asm7:"N mod m = k1-2 \<or> N mod m = k1-1" for N using w_cover asm7 by auto
 
-    have "\<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)" 
-      if asm10:"N mod m \<ge> 0 \<and> N mod m \<le>w" for N using c2 c3 asm10 
+    have "\<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)"
+      if asm10:"N mod m \<ge> 0 \<and> N mod m \<le>w" for N using c2 c3 asm10
       using \<open>\<And>N. 0 < N mod m \<and> int (N mod m) \<le> w \<Longrightarrow> \<exists>b r. r \<le> m - 3 \<and> [int N = b + int r]
       (mod int m) \<and> (b = b1 \<or> b = b2)\<close> by blast
-    hence c5:"\<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)" 
+    hence c5:"\<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)"
       if asm11:"N mod m \<ge> 0 \<and> N mod m \<le>k1-3" for N using w_cover using asm11 by force
 
-    have c6:"\<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)" 
-      if asm9:"(N mod m \<ge>0 \<and> N mod m \<le> k1-3) \<or> N mod m = k1-2 \<or> N mod m = k1-1" for N 
+    have c6:"\<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)"
+      if asm9:"(N mod m \<ge>0 \<and> N mod m \<le> k1-3) \<or> N mod m = k1-2 \<or> N mod m = k1-1" for N
       using c5 c4 asm9 by blast
 
-    hence c7:"\<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)" 
-      if asm12:"(N mod m \<ge>0 \<and> N mod m \<le> k1-3) \<or> N mod m = k1-2 \<or> N mod m = k1-1 \<or> 
+    hence c7:"\<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)"
+      if asm12:"(N mod m \<ge>0 \<and> N mod m \<le> k1-3) \<or> N mod m = k1-2 \<or> N mod m = k1-1 \<or>
  (N mod m \<ge> k1 \<and> N mod m \<le> m-1)" for N using asm12 c1 by blast
 
-    have "\<forall>N::nat. (N mod m \<ge>0 \<and> N mod m\<le> k1-3) \<or> N mod m = k1-2 \<or> N mod m = k1-1 \<or> 
- (N mod m \<ge> k1 \<and> N mod m \<le> m-1)" using k1_def 
-      by (smt (verit, best) Suc_pred' assms(1) bot_nat_0.extremum le_simps(2) mod_less_divisor 
+    have "\<forall>N::nat. (N mod m \<ge>0 \<and> N mod m\<le> k1-3) \<or> N mod m = k1-2 \<or> N mod m = k1-1 \<or>
+ (N mod m \<ge> k1 \<and> N mod m \<le> m-1)" using k1_def
+      by (smt (verit, best) Suc_pred' assms(1) bot_nat_0.extremum le_simps(2) mod_less_divisor
 not_numeral_le_zero of_nat_0_less_iff of_nat_le_0_iff)
 
     thus ?thesis using c7 by auto
   qed
 
   have second:"\<forall>N::nat. \<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)"
     if second_assum:"b1 mod m \<ge>0 \<and> b1 mod m \<le>2"
   proof -
     have case1:"\<forall>N::nat. \<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)"
       if case1_assum:"b1 mod m = 0"
     proof -
       have "\<exists>r::nat. (r \<le> m-3) \<and> [N = b1+r] (mod m)" if case1_1_assum:"N mod m \<le>m-3" for N
-        using case1_assum case1_1_assum 
+        using case1_assum case1_1_assum
         by (metis cong_add_rcancel_0 cong_mod_left cong_refl cong_sym_eq zmod_int)
-      hence case1_1:"\<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)" 
+      hence case1_1:"\<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)"
         if case1_1_assum:"N mod m \<le>m-3" for N using case1_1_assum by blast
 
       have "[N = b1+(m-2)] (mod m)" if case1_2_assum:"N mod m = m-2" for N using case1_2_assum
-        case1_assum by (metis (no_types, opaque_lifting) add.commute cong_add_lcancel_0 
+        case1_assum by (metis (no_types, opaque_lifting) add.commute cong_add_lcancel_0
             cong_mod_right of_nat_mod unique_euclidean_semiring_class.cong_def)
       hence "[N = b2+(m-4)] (mod m)" if case1_2_assum:"N mod m = m-2" for N using case1_2_assum assms(3)
         by (smt (verit, best) add_leD2 assms(1) int_ops(2) numeral_Bit0 of_nat_diff of_nat_numeral
             semiring_norm(172))
       hence "\<exists>r::nat. (r \<le> m-3) \<and> [N = b2+r] (mod m)" if case1_2_assum:"N mod m = m-2" for N
         using case1_2_assum
         by (meson diff_le_mono2 less_num_simps(2) numeral_le_iff verit_comp_simplify(15))
       hence case1_2:"\<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)"
         if case1_2_assum:"N mod m = m-2" for N using case1_2_assum by blast
 
       have "[N = b1+(m-1)] (mod m)" if case1_3_assum:"N mod m = m-1" for N using case1_3_assum
-        case1_assum by (metis (no_types, opaque_lifting) add.commute cong_add_lcancel_0 
+        case1_assum by (metis (no_types, opaque_lifting) add.commute cong_add_lcancel_0
             cong_mod_right of_nat_mod unique_euclidean_semiring_class.cong_def)
       hence "[N = b2+(m-3)] (mod m)" if case1_3_assum:"N mod m = m-1" for N using case1_3_assum assms(3)
-        by (smt (verit, best) assms(1) int_ops(2) int_ops(6) numeral_Bit0 numeral_Bit1 of_nat_mono 
+        by (smt (verit, best) assms(1) int_ops(2) int_ops(6) numeral_Bit0 numeral_Bit1 of_nat_mono
             of_nat_numeral semiring_norm(172))
       hence "\<exists>r::nat. (r \<le> m-3) \<and> [N = b2+r] (mod m)" if case1_3_assum:"N mod m = m-1" for N
         using case1_3_assum by blast
       hence case1_3:"\<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)"
         if case1_3_assum:"N mod m = m-1" for N using case1_3_assum by blast
 
       have "\<forall>N::nat. (N mod m = m-1) \<or> (N mod m = m-2) \<or> (N mod m \<le> m-3)"
-        by (smt (verit, ccfv_threshold) Suc_pred' assms(1) bot_nat_0.not_eq_extremum diff_diff_add 
-diff_is_0_eq' le_simps(2) mod_less_divisor nat_1_add_1 nat_less_le not_numeral_le_zero 
+        by (smt (verit, ccfv_threshold) Suc_pred' assms(1) bot_nat_0.not_eq_extremum diff_diff_add
+diff_is_0_eq' le_simps(2) mod_less_divisor nat_1_add_1 nat_less_le not_numeral_le_zero
 numeral.simps(3) semiring_norm(172))
       thus ?thesis using case1_1 case1_2 case1_3 by blast
     qed
 
     have case2:"\<forall>N::nat. \<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)"
       if case2_assum:"b1 mod m = 1"
     proof -
       have case2b2:"b2 mod m = 3" using case2_assum assms(3) by (smt (verit) assms(1) int_ops(2)
  mod_add_eq mod_pos_pos_trivial numeral_Bit0 of_nat_mono of_nat_numeral semiring_norm(172))
 
       have "\<exists>r::nat. (r\<le>m-3) \<and> [N = b2+r] (mod m)" if case2_1_assum:"N mod m = m-1" for N
       proof -
         have "[N = 3+(m-4)] (mod m)" using case2_1_assum
           by (metis (mono_tags, lifting) Suc_eq_plus1 Suc_numeral add_diff_cancel_left
              arithmetic_simps(1) arithmetic_simps(7) assms(1)mod_mod_trivial
              ordered_cancel_comm_monoid_diff_class.diff_add_assoc unique_euclidean_semiring_class.cong_def)
-        hence "[N = b2+(m-4)] (mod m)" using case2b2 
-          by (metis (mono_tags, lifting) Num.of_nat_simps(4) mod_add_left_eq 
+        hence "[N = b2+(m-4)] (mod m)" using case2b2
+          by (metis (mono_tags, lifting) Num.of_nat_simps(4) mod_add_left_eq
               of_nat_mod of_nat_numeral unique_euclidean_semiring_class.cong_def)
         thus ?thesis using le_diff_conv by fastforce
       qed
       hence case2_1:"\<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)"
         if case2_1_assum:"N mod m = m-1" for N using case2_1_assum by blast
 
       have "\<exists>r::nat. (r\<le>m-3) \<and> [N = b2+r] (mod m)" if case2_2_assum:"N mod m =0" for N
       proof -
         have "(3+(m-3)) mod m = 0" using assms(1) by fastforce
-        hence "(b2+(m-3)) mod m = 0" using case2b2 by (metis Num.of_nat_simps(1) 
+        hence "(b2+(m-3)) mod m = 0" using case2b2 by (metis Num.of_nat_simps(1)
               Num.of_nat_simps(4) mod_add_left_eq of_nat_mod of_nat_numeral)
-        thus ?thesis using case2_2_assum 
+        thus ?thesis using case2_2_assum
           by (metis int_ops(1) nat_le_linear of_nat_mod unique_euclidean_semiring_class.cong_def)
       qed
       hence case2_2:"\<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)"
         if case2_2_assum:"N mod m =0" for N using case2_2_assum by metis
 
-      have "\<exists>r::nat. (r \<le> m-3) \<and> [N = b1+r] (mod m)" if 
-        case2_3_assum:"N mod m \<le>m-2 \<and> N mod m \<ge>1" for N 
+      have "\<exists>r::nat. (r \<le> m-3) \<and> [N = b1+r] (mod m)" if
+        case2_3_assum:"N mod m \<le>m-2 \<and> N mod m \<ge>1" for N
       proof -
         have "\<exists>r::nat. (r\<le>m-3)\<and>((b1+r) mod m = l)" if asml:"l\<ge>1 \<and> l\<le>m-2" for l
         proof -
           define r where r_def:"r = l-1"
           from asml have r_range:"r\<ge>0 \<and> r\<le>m-3" using r_def by linarith
           have "(1+r) mod m = l" using asml r_def r_range by fastforce
           hence "(b1+r) mod m = l" using case2_assum
             by (metis Num.of_nat_simps(3) int_ops(9) mod_add_left_eq plus_1_eq_Suc)
           thus ?thesis using asml r_range by blast
         qed
         thus ?thesis using case2_3_assum
           by (metis case2_3_assum of_nat_mod unique_euclidean_semiring_class.cong_def)
       qed
       hence case2_3:"\<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)"
         if  case2_3_assum:"N mod m \<le>m-2 \<and> N mod m \<ge>1" for N using case2_3_assum by blast
 
-      have "\<forall>N::nat. N mod m = 0 \<or> (N mod m \<ge>1 \<and> N mod m \<le>m-1)" by (metis One_nat_def Suc_pred 
+      have "\<forall>N::nat. N mod m = 0 \<or> (N mod m \<ge>1 \<and> N mod m \<le>m-1)" by (metis One_nat_def Suc_pred
 assms(1) bot_nat_0.extremum_uniqueI leI less_Suc_eq_le mod_less_divisor not_numeral_le_zero)
-      hence "\<forall>N::nat. N mod m = 0 \<or> (N mod m \<ge>1 \<and> N mod m \<le>m-2) \<or> N mod m = m-1" 
-        by (smt (verit) arithmetic_simps(68) diff_diff_eq le_add_diff_inverse le_neq_implies_less le_simps(2) 
+      hence "\<forall>N::nat. N mod m = 0 \<or> (N mod m \<ge>1 \<and> N mod m \<le>m-2) \<or> N mod m = m-1"
+        by (smt (verit) arithmetic_simps(68) diff_diff_eq le_add_diff_inverse le_neq_implies_less le_simps(2)
            le_trans plus_1_eq_Suc)
       thus ?thesis using case2_1 case2_2 case2_3 by (metis \<open>\<And>N. N mod m \<le> m - 2 \<and> 1 \<le> N mod m
    \<Longrightarrow> \<exists>r\<le>m - 3. [int N = b1 + int r] (mod int m)\<close>)
     qed
 
     have case3:"\<forall>N::nat. \<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)"
       if case3_assum:"b1 mod m = 2"
     proof -
-      have case3b2:"b2 mod m = 4" using assms case3_assum by (smt (verit, ccfv_SIG)
- Euclidean_Division.pos_mod_sign dvd_mod_imp_dvd even_numeral int_ops(2) int_ops(4)
-mod_diff_eq mod_pos_pos_trivial nat_1_add_1 numeral_Bit0 of_nat_le_iff of_nat_numeral plus_1_eq_Suc)
+      have case3b2:"b2 mod m = 4"
+        using assms case3_assum
+        by (smt (verit, ccfv_SIG) Euclidean_Rings.pos_mod_sign dvd_mod_imp_dvd even_numeral int_ops(2)
+                int_ops(4) mod_diff_eq mod_pos_pos_trivial nat_1_add_1 numeral_Bit0 of_nat_le_iff
+                of_nat_numeral plus_1_eq_Suc)
 
       have "\<exists>r::nat. (r\<le>m-3)\<and> [N = b2+r] (mod m)" if case3_1_assum:"N mod m = 0 \<or> N mod m =1" for N
       proof -
         have "(4+(m-3)) mod m = (4+m-3) mod m" using assms(1) by auto
         have "(4+m-3) mod m = (1+m) mod m" by simp
         hence "(4+(m-3)) mod m = 1" using \<open>(4+(m-3)) mod m = (4+m-3) mod m\<close>
-          by (smt (verit, best) Euclidean_Division.pos_mod_bound add_lessD1 arith_special(2) assms(1) case3b2
-              landau_product_preprocess(4) mod_add_self2 mod_less numeral_Bit0 of_nat_numeral order_le_less) 
-        hence caseone:"(b2+(m-3)) mod m = 1" using case3b2 
+          by (smt (verit, best) Euclidean_Rings.pos_mod_bound add_lessD1 arith_special(2) assms(1) case3b2
+              landau_product_preprocess(4) mod_add_self2 mod_less numeral_Bit0 of_nat_numeral order_le_less)
+        hence caseone:"(b2+(m-3)) mod m = 1" using case3b2
           by (metis Num.of_nat_simps(2) Num.of_nat_simps(4) mod_add_left_eq of_nat_mod of_nat_numeral)
 
         have "(4+(m-4)) mod m = 0" using assms(1) by auto
-        hence casezero:"(b2+(m-4)) mod m = 0" using case3b2 
+        hence casezero:"(b2+(m-4)) mod m = 0" using case3b2
           by (metis (full_types) Num.of_nat_simps(1) Num.of_nat_simps(4) mod_add_left_eq of_nat_mod of_nat_numeral)
 
-        show ?thesis using caseone casezero case3_1_assum 
-          by (metis cong_int cong_mod_right cong_refl diff_le_mono2 nat_le_linear numeral_le_iff 
+        show ?thesis using caseone casezero case3_1_assum
+          by (metis cong_int cong_mod_right cong_refl diff_le_mono2 nat_le_linear numeral_le_iff
               of_nat_0 of_nat_1 semiring_norm(69) semiring_norm(72))
       qed
       hence case3_1:"\<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)"
         if case3_1_assum:"N mod m = 0 \<or> N mod m =1" for N using case3_1_assum by metis
 
       have "\<exists>r::nat.(r\<le>m-3)\<and> [N = b1+r] (mod m)" if case3_2_assum:"N mod m \<ge>2\<and>N mod m \<le> m-1" for N
       proof -
         have "\<exists>r::nat. (r\<le>m-3)\<and>((b1+r) mod m = l)" if asml1:"l\<ge>2 \<and> l\<le>m-1" for l
         proof -
           define r1 where r1_def:"r1 = l-2"
           from asml1 have r1_range:"r1\<ge>0 \<and> r1\<le>m-2" using r1_def by linarith
           have "(2+r1) mod m = l" using asml1 r1_def r1_range by fastforce
           hence "(b1+r1) mod m = l" using case3_assum
             by (metis Num.of_nat_simps(4) mod_add_left_eq of_nat_mod of_nat_numeral)
           thus ?thesis using asml1 r1_range by (metis One_nat_def diff_diff_add diff_le_mono
                 nat_1_add_1 numeral_3_eq_3 plus_1_eq_Suc r1_def)
         qed
         thus ?thesis using case3_2_assum
           by (metis case3_2_assum of_nat_mod unique_euclidean_semiring_class.cong_def)
       qed
       hence case3_2:"\<exists>b::int. \<exists>r::nat. (r \<le> m-3) \<and> [N=b+r] (mod m) \<and> (b = b1 \<or> b = b2)"
         if case3_2_assum:"N mod m \<ge>2\<and>N mod m \<le> m-1" for N using case3_2_assum by blast
 
-      have "\<forall>N::nat. N mod m = 0 \<or> (N mod m \<ge>1 \<and> N mod m \<le>m-1)" by (metis Suc_pred' assms(1) 
+      have "\<forall>N::nat. N mod m = 0 \<or> (N mod m \<ge>1 \<and> N mod m \<le>m-1)" by (metis Suc_pred' assms(1)
 bot_nat_0.not_eq_extremum less_one mod_Suc_le_divisor rel_simps(76) verit_comp_simplify1(3))
-      hence "\<forall>N::nat. N mod m = 0 \<or> N mod m = 1 \<or> (N mod m \<ge>2 \<and> N mod m \<le>m-1)" 
+      hence "\<forall>N::nat. N mod m = 0 \<or> N mod m = 1 \<or> (N mod m \<ge>2 \<and> N mod m \<le>m-1)"
         by (metis Suc_eq_plus1 le_neq_implies_less le_simps(3) nat_1_add_1)
 
       thus ?thesis using case3_1 case3_2 by blast
     qed
 
     show ?thesis using case1 case2 case3 using that by fastforce
   qed
 
   show ?thesis using first second using assms(1) by force
 qed
 
-text\<open>The strong form of Cauchy's polygonal number theorem shows for a natural number $N$ satisfying 
-certain conditions, it may be written as the sum of $m+1$ polygonal numbers of order $m+2$, at most four 
+text\<open>The strong form of Cauchy's polygonal number theorem shows for a natural number $N$ satisfying
+certain conditions, it may be written as the sum of $m+1$ polygonal numbers of order $m+2$, at most four
 of which are different from 0 or 1. This corresponds to Theorem 1.9 in \cite{nathanson1996}.\<close>
 
 theorem Strong_Form_of_Cauchy_Polygonal_Number_Theorem_1:
   fixes m N :: nat
   assumes "m\<ge>4"
   assumes "N\<ge>108*m"
   shows "\<exists> xs :: nat list. (length xs = m+1) \<and> (sum_list xs = N) \<and> (\<forall>k\<le>3. \<exists>a. xs! k = polygonal_number m a)
-  \<and> (\<forall> k \<in> {4..m} . xs! k = 0 \<or> xs! k = 1)" 
+  \<and> (\<forall> k \<in> {4..m} . xs! k = 0 \<or> xs! k = 1)"
 
 proof -
   define L where L_def:"L = (2/3 + sqrt (8*N/m - 8)) - (1/2 + sqrt (6*N/m - 3))"
   from assms L_def have "L>4" using interval_length_greater_than_four
     apply(rule_tac N = "of_nat N" and m = "of_nat m" in interval_length_greater_than_four)
     by auto
   define c1 where c1_def:"c1 = \<lceil>1/2 + sqrt (6*N/m - 3)\<rceil>"
   define c2 where c2_def:"c2 = c1+1"
   define c3 where c3_def:"c3 = c1+2"
   define c4 where c4_def:"c4 = c1+3"
   from \<open>L>4\<close> c1_def c2_def c3_def c4_def L_def have "c4<(2/3 + sqrt (8*N/m - 8))" by linarith
 
   have "N/m \<ge> 108" using assms using le_divide_eq by fastforce
   hence "sqrt(6*N/m - 3)\<ge>1" by simp
   hence "1/2 + sqrt(6*N/m - 3) \<ge>1" by linarith
   hence "c1 \<ge>1" using c1_def by simp
 
-  obtain b1 b2 where bproperties:"{b1, b2} \<subseteq> {c1, c2, c3, c4} \<and> (b2 = b1+2) \<and> odd b1" 
-    using two_consec_odd c1_def c2_def c3_def c4_def by (metis (no_types, opaque_lifting) Groups.add_ac(2) 
+  obtain b1 b2 where bproperties:"{b1, b2} \<subseteq> {c1, c2, c3, c4} \<and> (b2 = b1+2) \<and> odd b1"
+    using two_consec_odd c1_def c2_def c3_def c4_def by (metis (no_types, opaque_lifting) Groups.add_ac(2)
 empty_subsetI even_plus_one_iff insert_commute insert_mono nat_arith.add1 numeral.simps(2) numeral.simps(3))
   have b1andb2:"odd b1 \<and> b2 = b1+2" using bproperties by auto
   have b1pos:"b1 \<ge>1" using \<open>c1\<ge>1\<close> c2_def c3_def c4_def bproperties by auto
   hence b2pos:"b2 \<ge>3" using bproperties by simp
   have b2odd:"odd b2" using bproperties by simp
-  
+
   obtain b r where b_r:"r\<le>m-3 \<and> (b = b1 \<or> b = b2) \<and> [int N = b+r] (mod m)" using b1andb2 assms(1)
       cong_classes by meson
   have bpos:"b\<ge>1" using b1pos b2pos b_r by auto
   have bodd:"odd b" using b_r bproperties by auto
 
   define a where a_def:"a = b+2*(N-b-r) div m"
   have m_div_num:"m dvd (N-b-r)" using b_r
     by (simp add: diff_diff_add mod_eq_dvd_iff unique_euclidean_semiring_class.cong_def)
   hence "(N-b-r)/m = (N-b-r) div m" by (simp add: real_of_int_div)
-  hence a_def1:"a = b+2*(N-b-r)/m" using a_def by (metis \<open>int m dvd int N - b - int r\<close> 
+  hence a_def1:"a = b+2*(N-b-r)/m" using a_def by (metis \<open>int m dvd int N - b - int r\<close>
         dvd_add_right_iff mult_2 of_int_add of_int_of_nat_eq real_of_int_div)
   have "N-m>0" using assms by linarith
-  hence "N-r>0" using b_r by force 
+  hence "N-r>0" using b_r by force
   hence "(N-b-r) = (N-r)-b" by linarith
   hence "(N-b-r)/m = (N-r)/m - b/m" by (metis diff_divide_distrib int_of_reals(3) of_int_of_nat_eq)
   hence "a = b+2*((N-r)/m - b/m)" using a_def1 by (metis int_of_reals(6) of_int_mult times_divide_eq_right)
   hence a_def2:"a = b- b*2/m+2*(N-r)/m " by simp
   have "b*(1-2/m) = b*1-b*(2/m)" by (simp add: Rings.ring_distribs(4))
   hence a_def3:"a = b*(1-2/m) + 2*(N-r)/m" using a_def2 by simp
   have "1-2/m>0" using assms(1) by simp
   hence size1:"b*(1-2/m)>0" using bpos by simp
   have "N-r>0" using b_r assms by auto
   hence size2:"2*(N-r)/m>0" using assms(1) by simp
-  have apos:"a\<ge>1" using size1 size2 a_def3 by simp 
+  have apos:"a\<ge>1" using size1 size2 a_def3 by simp
 
   have "odd (b+2*(N-b-r) div m)" using m_div_num b_r b2odd bproperties
     by (metis div_mult_swap zdvd_reduce)
   hence aodd:"odd a" using a_def by simp
 
   from a_def1 have "a-b = 2*(N-b-r)/m" by simp
   hence "m*(a-b)/2 = N-b-r" using assms(1) by simp
   hence N_expr:"N = r+b+m*(a-b)/2" by simp
 
   have "b1 \<ge> c1" using bproperties c2_def c3_def c4_def by force
   hence "b1 \<ge> 1/2 + sqrt (6*N/m - 3)" using c1_def using ceiling_le_iff by blast
   have b_ineq1:"b \<ge> 1/2 + sqrt (6*N/m - 3)" using b_r bproperties
-    using \<open>1 / 2 + sqrt (real (6 * N) / real m - 3) \<le> real_of_int b1\<close> by fastforce 
+    using \<open>1 / 2 + sqrt (real (6 * N) / real m - 3) \<le> real_of_int b1\<close> by fastforce
 
   have "b2 \<le> c4" using bproperties c1_def c2_def c3_def c4_def by fastforce
   hence "b2 \<le> (2/3 + sqrt (8*N/m - 8))"
     using \<open>real_of_int c4 < 2 / 3 + sqrt (real (8 * N) / real m - 8)\<close> by linarith
   hence b_ineq2:"b\<le>(2/3 + sqrt (8*N/m - 8))" using b_r bproperties by linarith
 
   define Nr where "Nr = real_of_nat N"
   define mr where "mr = real m"
   define ar where "ar = real_of_int a"
   define br where "br = real_of_int b"
   define rr where "rr = real_of_nat r"
   from assms(1) have "mr \<ge>3" using mr_def by auto
   from assms(2) have "N\<ge>2*m" by simp
   hence "Nr \<ge> 2*mr" using Nr_def mr_def \<open>N \<ge> 2 * m\<close> by auto
   moreover have "br\<ge>0" using br_def bpos by auto
   moreover have "mr\<ge>3" using mr_def assms by auto
   moreover have "ar\<ge>0" using ar_def apos by auto
   moreover have "rr\<ge>0" using rr_def b_r by auto
   moreover have "mr > rr" using mr_def rr_def b_r assms(1) by linarith
   moreover have "Nr = mr*(ar-br)/2+br+rr" using Nr_def mr_def ar_def br_def N_expr rr_def by auto
   moreover have "1/2+sqrt(6*Nr/mr-3)\<le>br \<and> br\<le>2/3+sqrt(8*Nr/mr-8)" using Nr_def mr_def br_def b_ineq1 b_ineq2 by auto
   ultimately have "br^2<4*ar \<and> 3*ar<br^2+2*br+4" using Cauchy_lemma by auto
-  hence real_ineq:"(real_of_int b)^2 < 4*(real_of_int a) \<and> 3*(real_of_int a) < (real_of_int b)^2 + 2*(real_of_int b) + 4" 
+  hence real_ineq:"(real_of_int b)^2 < 4*(real_of_int a) \<and> 3*(real_of_int a) < (real_of_int b)^2 + 2*(real_of_int b) + 4"
     using br_def ar_def by auto
   hence int_ineq1: "b^2<4*a" using of_int_less_iff by fastforce
   from real_ineq have int_ineq2: "3*a<b^2+2*b+4" using of_int_less_iff by fastforce
 
   have con1:"nat a \<ge>1" using apos by auto
   have con2:"nat b \<ge>1" using bpos by auto
   have con3:"odd (nat a)" using aodd apos even_nat_iff by auto
   have con4:"odd (nat b)" using bodd bpos even_nat_iff by auto
   have "(nat b)^2 = b^2" using \<open>nat b \<ge>1\<close> by auto
   hence con5:"(nat b)^2<4*(nat a)" using int_ineq1 by linarith
   have con6:"3*(nat a)<(nat b)^2+2*(nat b)+4" using \<open>(nat b)^2 = b^2\<close> int_ineq2 by linarith
   obtain s t u v where stuv:"s \<ge> 0 \<and> t \<ge> 0 \<and> u \<ge> 0 \<and> v \<ge> 0 \<and> int(nat a) = s^2 + t^2 + u^2 + v^2 \<and>
   int(nat b) = s+t+u+v" using four_nonneg_int_sum con1 con2 con3 con4 con5 con6 by presburger
   have a_expr:"a = s^2 + t^2 + u^2 + v^2" using apos stuv by linarith
   have b_expr:"b = s+t+u+v" using bpos stuv by linarith
 
   from N_expr have "N = m/2*(s^2-s+t^2-t+u^2-u+v^2-v)+r+(s+t+u+v)" using a_expr b_expr by simp
   hence N_expr2:"N = m/2*(s^2-s)+ m/2*(t^2-t)+ m/2*(u^2-u)+ m/2*(v^2-v)+ r+(s+t+u+v)"
     by (metis (no_types, opaque_lifting) add_diff_eq nat_distrib(2) of_int_add)
   have s_div2:"m/2*(s^2-s) = m*(s^2-s) div 2" using real_of_int_div by auto
   have t_div2:"m/2*(t^2-t) = m*(t^2-t) div 2" using real_of_int_div by auto
   have u_div2:"m/2*(u^2-u) = m*(u^2-u) div 2" using real_of_int_div by auto
   have v_div2:"m/2*(v^2-v) = m*(v^2-v) div 2" using real_of_int_div by auto
   have N_expr3:"N = (m*(s^2-s) div 2+s)+(m*(t^2-t) div 2+t)+(m*(u^2-u) div 2+u)+(m*(v^2-v) div 2+v)+r"
     using s_div2 t_div2 u_div2 v_div2 N_expr2 by simp
 
   define sn where "sn = nat s"
   define tn where "tn = nat t"
   define un where "un = nat u"
   define vn where "vn = nat v"
-  have seqsn:"s^2-s = sn^2 - sn" using stuv sn_def 
+  have seqsn:"s^2-s = sn^2 - sn" using stuv sn_def
     by (metis int_nat_eq le_refl of_nat_diff of_nat_power power2_nat_le_imp_le)
   have teqtn:"t^2-t = tn^2 - tn" using stuv tn_def
     by (metis int_nat_eq le_refl of_nat_diff of_nat_power power2_nat_le_imp_le)
-  have uequn:"u^2-u = un^2 - un" using stuv un_def 
+  have uequn:"u^2-u = un^2 - un" using stuv un_def
     by (metis int_nat_eq le_refl of_nat_diff of_nat_power power2_nat_le_imp_le)
-  have veqvn:"v^2-v = vn^2 - vn" using stuv vn_def 
+  have veqvn:"v^2-v = vn^2 - vn" using stuv vn_def
     by (metis int_nat_eq le_refl of_nat_diff of_nat_power power2_nat_le_imp_le)
 
-  from N_expr3 have 
+  from N_expr3 have
     "N = (m*(sn^2-sn) div 2+s)+(m*(tn^2-tn) div 2+t)+(m*(un^2-un) div 2+u)+(m*(vn^2-vn) div 2+ v)+r"
-    using seqsn teqtn uequn veqvn by (metis (mono_tags, lifting) int_ops(2) int_ops(4) int_ops(7) 
+    using seqsn teqtn uequn veqvn by (metis (mono_tags, lifting) int_ops(2) int_ops(4) int_ops(7)
         numeral_Bit0 numeral_code(1) plus_1_eq_Suc zdiv_int)
-  hence "N = (m*(sn^2-sn) div 2+sn)+(m*(tn^2-tn) div 2+tn)+(m*(un^2-un) div 2+un)+(m*(vn^2-vn) div 2+ v)+r" 
+  hence "N = (m*(sn^2-sn) div 2+sn)+(m*(tn^2-tn) div 2+tn)+(m*(un^2-un) div 2+un)+(m*(vn^2-vn) div 2+ v)+r"
     using sn_def tn_def un_def  stuv int_nat_eq int_ops(5) by presburger
   hence "N = (m*(sn^2-sn) div 2+sn)+(m*(tn^2-tn) div 2+tn)+(m*(un^2-un) div 2+un)+(m*(vn^2-vn) div 2+ vn)+r"
     using vn_def stuv by (smt (verit, del_insts) Num.of_nat_simps(4) int_nat_eq of_nat_eq_iff)
   hence "N = (m* sn*(sn-1) div 2+sn)+(m*tn*(tn-1) div 2+tn)+(m*un*(un-1) div 2+un)+(m* vn*(vn-1) div 2+ vn)+r"
     by (smt (verit, ccfv_threshold) more_arith_simps(11) mult.right_neutral power2_eq_square right_diff_distrib')
   hence N_expr4:"N = polygonal_number m sn + polygonal_number m tn + polygonal_number m un + polygonal_number m vn +r"
     using Polygonal_Number_Theorem_Gauss.polygonal_number_def by presburger
 
   define T where T_def:"T = [polygonal_number m sn,polygonal_number m tn,polygonal_number m un,polygonal_number m vn]"
   define ones where ones_def:"ones = replicate r (1::nat)"
   define zeros where zeros_def:"zeros = replicate (m+1-4-r) (0::nat)"
   define final where final_def:"final = T@ones@zeros"
 
   have "m+1-4-r\<ge>0" using assms(1) b_r by force
-  hence "4+r+(m+1-4-r) = m+1" using assms(1) b_r by force 
+  hence "4+r+(m+1-4-r) = m+1" using assms(1) b_r by force
   have "length final = 4+r+(m+1-4-r)" using final_def T_def ones_def zeros_def by auto
   hence final_length:"length final = m+1" using \<open>4+r+(m+1-4-r) = m+1\<close> by simp
   have T_sum:"sum_list T = polygonal_number m sn + polygonal_number m tn + polygonal_number m un + polygonal_number m vn" by (simp add: T_def)
   have ones_sum:"sum_list ones = r" using ones_def by (simp add: sum_list_replicate)
   have zeros_sum:"sum_list zeros = 0" using zeros_def by simp
   have "sum_list final = sum_list T + sum_list ones + sum_list zeros" using final_def by simp
   hence final_sum:"sum_list final = N" using N_expr4 by (simp add: T_sum ones_sum zeros_sum)
 
   have final_0th:"final! 0 = polygonal_number m sn" using final_def T_def by simp
   have final_1st:"final! 1 = polygonal_number m tn" using final_def T_def by simp
   have final_2nd:"final! 2 = polygonal_number m un" using final_def T_def by simp
   have final_3rd:"final! 3 = polygonal_number m vn" using final_def T_def by simp
 
   have first_four:"\<forall>k\<le>3. \<exists>a. final! k = polygonal_number m a" using final_0th final_1st final_2nd final_3rd
-    by (metis Suc_eq_plus1 add_leD2 arith_simps(50) le_simps(2) numeral_Bit0 numeral_Bit1 
+    by (metis Suc_eq_plus1 add_leD2 arith_simps(50) le_simps(2) numeral_Bit0 numeral_Bit1
         numeral_One verit_comp_simplify1(3) verit_la_disequality)
-  
+
   have "length T = 4" using T_def by simp
   have "\<forall>k<length (ones@zeros). (ones@zeros)! k =1 \<or>  (ones@zeros)! k =0" using ones_def zeros_def
     by (simp add: nth_append)
-  hence "final! k = 1 \<or> final! k = 0" if "k\<ge>4 \<and> k<(length final)" for k 
+  hence "final! k = 1 \<or> final! k = 0" if "k\<ge>4 \<and> k<(length final)" for k
     using \<open>length T = 4\<close> final_def that by (metis add_less_cancel_left le_add_diff_inverse
         length_append nth_append verit_comp_simplify1(3))
   hence other_terms:"\<forall> k \<in> {4..m} . final! k = 0 \<or> final! k = 1" using final_length
     by (metis Suc_eq_plus1 atLeastAtMost_iff le_simps(2))
 
   show ?thesis using final_length final_sum first_four other_terms by auto
 qed
- 
+
 
 theorem Strong_Form_of_Cauchy_Polygonal_Number_Theorem_2:
   fixes N :: nat
   assumes "N\<ge>324"
   shows "\<exists> p1 p2 p3 p4 r ::nat. N = p1+p2+p3+p4+r \<and> (\<exists>k1. p1 = polygonal_number 3 k1) \<and> (\<exists>k2. p2 = polygonal_number 3 k2)
 \<and> (\<exists>k3. p3 = polygonal_number 3 k3) \<and> (\<exists>k4. p4 = polygonal_number 3 k4) \<and> (r = 0 \<or> r = 1)"
 
 proof -
   define L where L_def:"L = (2/3 + sqrt (8*N/3 - 8)) - (1/2 + sqrt (6*N/3 - 3))" (*Now m = 3*)
   from assms L_def have "L>4" using interval_length_greater_than_four
     apply -
     apply(rule interval_length_greater_than_four[where N = "of_nat N" and m = "of_nat 3"])
     by auto
   define c1 where c1_def:"c1 = \<lceil>1/2 + sqrt (6*N/3 - 3)\<rceil>"
   define c2 where c2_def:"c2 = c1+1"
   define c3 where c3_def:"c3 = c1+2"
   define c4 where c4_def:"c4 = c1+3"
   from \<open>L>4\<close> c1_def c2_def c3_def c4_def L_def have "c4<(2/3 + sqrt (8*N/3 - 8))" by linarith
 
   define Nn where "Nn = int N"
   have "c4<(2/3 + sqrt (8*Nn/3 - 8))" using Nn_def \<open>c4<(2/3 + sqrt (8*N/3 - 8))\<close> by simp
-  have Nn3:"(Nn-3)^2 - (sqrt (8*Nn/3 - 8))^2 = Nn^2-3*Nn-3*Nn+9 - (sqrt (8*Nn/3 - 8))^2" 
+  have Nn3:"(Nn-3)^2 - (sqrt (8*Nn/3 - 8))^2 = Nn^2-3*Nn-3*Nn+9 - (sqrt (8*Nn/3 - 8))^2"
     using assms Nn_def power2_diff by (simp add: power2_eq_square algebra_simps)
   have "(Nn-3)^2 - (sqrt (8*Nn/3 - 8))^2 = Nn^2-3*Nn-3*Nn+9 - (8*Nn/3 - 8)" using assms Nn_def Nn3 by fastforce
   hence "(Nn-3)^2 - (sqrt (8*Nn/3 - 8))^2 = Nn^2-6*Nn+9-8*Nn/3 +8" by linarith
   hence Nn4:"(Nn-3)^2 - (sqrt (8*Nn/3 - 8))^2 = Nn*(Nn-26/3)+17" by (simp add: Rings.ring_distribs(4) power2_eq_square)
   have "Nn*(Nn-26/3)+17>17" using assms Nn_def by auto
   hence "(Nn-3)^2 - (sqrt (8*Nn/3 - 8))^2 > 0" using Nn4 by auto
   hence "Nn-3 > sqrt (8*Nn/3 - 8)" using assms Nn_def by (simp add: real_less_lsqrt)
   hence "Nn-2 > sqrt (8*Nn/3 - 8)+2/3" by linarith
   hence "N > c4" using Nn_def \<open>c4<(2/3 + sqrt (8*Nn/3 - 8))\<close> by simp
 
   have "N/3 \<ge> 108" using assms using le_divide_eq by fastforce
   hence "sqrt(6*N/3 - 3)\<ge>1" by simp
   hence "1/2 + sqrt(6*N/3 - 3) \<ge>1" by linarith
   hence "c1 \<ge>1" using c1_def by simp
 
-  obtain b1 b2 where bproperties:"{b1, b2} \<subseteq> {c1, c2, c3, c4} \<and> (b2 = b1+2) \<and> odd b1" 
-    using two_consec_odd c1_def c2_def c3_def c4_def by (metis (no_types, opaque_lifting) Groups.add_ac(2) 
+  obtain b1 b2 where bproperties:"{b1, b2} \<subseteq> {c1, c2, c3, c4} \<and> (b2 = b1+2) \<and> odd b1"
+    using two_consec_odd c1_def c2_def c3_def c4_def by (metis (no_types, opaque_lifting) Groups.add_ac(2)
 empty_subsetI even_plus_one_iff insert_commute insert_mono nat_arith.add1 numeral.simps(2) numeral.simps(3))
   have b1andb2:"odd b1 \<and> b2 = b1+2" using bproperties by auto
   have b1pos:"b1 \<ge>1" using \<open>c1\<ge>1\<close> c2_def c3_def c4_def bproperties by auto
   hence b2pos:"b2 \<ge>3" using bproperties by simp
   have b2odd:"odd b2" using bproperties by simp
   define b1n where "b1n = nat b1"
   define b2n where "b2n = nat b2"
 
   from b1n_def b1pos have "b1n mod 3 = b1 mod 3" using int_ops(9) by force
   from b2n_def b2pos have "b2n mod 3 = b2 mod 3" using int_ops(9) by force
 
   have b_and_r:"\<exists>b r::nat. [N = b+r] (mod 3) \<and> (b = b1n \<or> b = b2n) \<and> (r = 0 \<or> r = 1)"
   proof -
-    have case1:"\<exists>b r::nat. [N = b+r] (mod 3) \<and> (b = b1n \<or> b = b2n) \<and> (r = 0 \<or> r = 1)" 
+    have case1:"\<exists>b r::nat. [N = b+r] (mod 3) \<and> (b = b1n \<or> b = b2n) \<and> (r = 0 \<or> r = 1)"
       if asm1:"b1 mod 3 = 0"
     proof -
       have "b1n mod 3 = 0" using asm1 \<open>b1n mod 3 = b1 mod 3\<close> by simp
       hence "b2n mod 3 = 2" using \<open>b2n mod 3 = b2 mod 3\<close> bproperties asm1 by fastforce
-      have case1_1:"[0 = b1n+0] (mod 3)" using \<open>b1n mod 3 = 0\<close> 
+      have case1_1:"[0 = b1n+0] (mod 3)" using \<open>b1n mod 3 = 0\<close>
         by (metis mod_0 nat_arith.rule0 unique_euclidean_semiring_class.cong_def)
       have case1_2:"[1 = b1n+1] (mod 3)" using \<open>b1n mod 3 = 0\<close>
         by (metis \<open>[0 = b1n + 0] (mod 3)\<close> add.commute cong_add_lcancel_0_nat cong_sym)
       have case1_3:"[2 = b2n+0] (mod 3)" using \<open>b2n mod 3 = 2\<close>
         by (simp add: unique_euclidean_semiring_class.cong_def)
       have "\<forall>N::nat. N mod 3 = 0 \<or> N mod 3 \<ge> 1" by linarith
       hence "\<forall>N::nat. N mod 3 = 0 \<or> N mod 3 = 1 \<or> N mod 3 = 2" by linarith
       hence "\<forall>N. \<exists>b r::nat. [N = b+r] (mod 3) \<and> (b = b1n \<or> b = b2n) \<and> (r = 0 \<or> r = 1)"
         if asm1:"b1 mod 3 = 0" using case1_1 case1_2 case1_3 by (metis cong_mod_left)
       thus ?thesis using asm1 by auto
     qed
 
-    have case2:"\<exists>b r::nat. [N = b+r] (mod 3) \<and> (b = b1n \<or> b = b2n) \<and> (r = 0 \<or> r = 1)" 
+    have case2:"\<exists>b r::nat. [N = b+r] (mod 3) \<and> (b = b1n \<or> b = b2n) \<and> (r = 0 \<or> r = 1)"
       if asm2:"b1 mod 3 = 1"
     proof -
       have "b1n mod 3 = 1" using asm2 \<open>b1n mod 3 = b1 mod 3\<close> by simp
       hence "b2n mod 3 = 0" using \<open>b2n mod 3 = b2 mod 3\<close> bproperties asm2
-        by (smt (verit, best) Euclidean_Division.pos_mod_bound Euclidean_Division.pos_mod_sign
+        by (smt (verit, best) Euclidean_Rings.pos_mod_bound Euclidean_Rings.pos_mod_sign
             int_ops(1) mod_diff_eq mod_pos_pos_trivial of_nat_eq_iff)
-      have case2_1:"[0 = b2n+0] (mod 3)" using \<open>b2n mod 3 = 0\<close> 
+      have case2_1:"[0 = b2n+0] (mod 3)" using \<open>b2n mod 3 = 0\<close>
         by (metis mod_0 nat_arith.rule0 unique_euclidean_semiring_class.cong_def)
       have case2_2:"[1 = b1n+0] (mod 3)" using \<open>b1n mod 3 = 1\<close>
         by (simp add: unique_euclidean_semiring_class.cong_def)
       have case2_3:"[2 = b1n+1] (mod 3)" using \<open>b1n mod 3 = 1\<close>
         by (metis case2_2 cong_add_rcancel_nat nat_1_add_1 nat_arith.rule0)
       have "\<forall>N::nat. N mod 3 = 0 \<or> N mod 3 \<ge> 1" by linarith
       hence "\<forall>N::nat. N mod 3 = 0 \<or> N mod 3 = 1 \<or> N mod 3 = 2" by linarith
       hence "\<forall>N. \<exists>b r::nat. [N = b+r] (mod 3) \<and> (b = b1n \<or> b = b2n) \<and> (r = 0 \<or> r = 1)"
         if asm2:"b1 mod 3 = 1" using case2_1 case2_2 case2_3 by (metis cong_mod_left)
       thus ?thesis using asm2 by auto
     qed
 
-    have case3:"\<exists>b r::nat. [N = b+r] (mod 3) \<and> (b = b1n \<or> b = b2n) \<and> (r = 0 \<or> r = 1)" 
+    have case3:"\<exists>b r::nat. [N = b+r] (mod 3) \<and> (b = b1n \<or> b = b2n) \<and> (r = 0 \<or> r = 1)"
       if asm3:"b1 mod 3 = 2"
     proof -
       have "b1n mod 3 = 2" using asm3 \<open>b1n mod 3 = b1 mod 3\<close> by simp
       have "(b1+2) mod 3 = (2+2) mod 3" using asm3 by (metis Groups.add_ac(2) mod_add_right_eq)
       hence "b2n mod 3 = 1" using \<open>b2n mod 3 = b2 mod 3\<close> bproperties by simp
       have case3_1:"[0 = b1n+1] (mod 3)" using \<open>b1n mod 3 = 2\<close>
         by (metis One_nat_def add.commute mod_0 mod_add_right_eq mod_self nat_1_add_1 numeral_3_eq_3
             plus_1_eq_Suc unique_euclidean_semiring_class.cong_def)
       have case3_2:"[1 = b2n+0] (mod 3)" using \<open>b2n mod 3 = 1\<close>
         by (simp add: unique_euclidean_semiring_class.cong_def)
       have case3_3:"[2 = b1n+0] (mod 3)" using \<open>b1n mod 3 = 2\<close>
         by (simp add: unique_euclidean_semiring_class.cong_def)
       have "\<forall>N::nat. N mod 3 = 0 \<or> N mod 3 \<ge> 1" by linarith
       hence "\<forall>N::nat. N mod 3 = 0 \<or> N mod 3 = 1 \<or> N mod 3 = 2" by linarith
       hence "\<forall>N. \<exists>b r::nat. [N = b+r] (mod 3) \<and> (b = b1n \<or> b = b2n) \<and> (r = 0 \<or> r = 1)"
         if asm3:"b1 mod 3 = 2" using case3_1 case3_2 case3_3 by (metis cong_mod_left)
       thus ?thesis using asm3 by auto
     qed
 
     have "b1 mod 3 = 0 \<or> b1 mod 3 = 1 \<or> b1 mod 3 = 2" by auto
     thus ?thesis using case1 case2 case3 by auto
   qed
 
-  obtain b r where b_r:"[N = b+r] (mod 3) \<and> (b = b1n \<or> b = b2n) \<and> (r = 0 \<or> r = 1)" 
+  obtain b r where b_r:"[N = b+r] (mod 3) \<and> (b = b1n \<or> b = b2n) \<and> (r = 0 \<or> r = 1)"
     using b_and_r by auto
 
   have bpos:"b\<ge>1" using b1pos b2pos b_r b1n_def b2n_def by auto
-  have bodd:"odd b" 
+  have bodd:"odd b"
     using b_r bproperties by (metis b1n_def b2n_def b2odd bpos even_nat_iff nat_eq_iff2 rel_simps(45))
 
   define a where a_def:"a = b+2*(N-b-r) div 3"
   have "int b1n = b1" using b1n_def b1pos by linarith
   have "int b2n = b2" using b2n_def b2pos by linarith
   have m_div_num:"3 dvd (N-b-r)" using b_r
     by (metis cong_altdef_nat diff_diff_left diff_is_0_eq' dvd_0_right nat_le_linear)
   hence a_def1:"a = b+2*(N-b-r)/3" using a_def m_div_num real_of_nat_div by auto
   from \<open>N>c4\<close> have "N>b" using b_r bproperties b1n_def b2n_def
     by (smt (verit, del_insts) \<open>int b1n = b1\<close> \<open>int b2n = b2\<close> c2_def c3_def c4_def empty_iff insert_iff insert_subset of_nat_less_imp_less)
   hence "(N-b-r)/3 = (N-r)/3 - b/3" using \<open>b < N\<close> b_r by force
   hence "a = b- b*2/3+2*(N-r)/3" using a_def1 by linarith
   hence a_def3:"a = b*(1-2/3) + 2*(N-r)/3" by simp
 
   have size1:"b*(1-2/3)>0" using bpos by simp
   have "N-r>0" using b_r assms by auto
   hence size2:"2*(N-r)/3>0" using assms(1) by simp
-  have apos:"a\<ge>1" using size1 size2 a_def3 by simp 
+  have apos:"a\<ge>1" using size1 size2 a_def3 by simp
 
   have "odd (b+2*(N-b-r) div 3)" using m_div_num b_r b2odd bproperties by (simp add: bodd mult_2)
   hence aodd:"odd a" using a_def by simp
   from a_def1 have "a-b = 2*(N-b-r)/3" by simp
   hence "(a-b)/2 = (N-b-r)/3" by simp
   hence "3*(a-b)/2 = N-b-r"  by simp
   have "N-b-r\<ge>0" using b_r by simp
   hence N_expr:"N = r+b+3*(a-b)/2" using \<open>N-b-r\<ge>0\<close>  \<open>b < N\<close> b_r \<open>real (3 * (a - b)) / 2 = real (N - b - r)\<close> by linarith
   from a_def \<open>N-b-r\<ge>0\<close> have "a\<ge>b" using a_def le_add1 by blast
 
   have "b1 \<ge> c1" using bproperties c2_def c3_def c4_def by force
   hence "b1 \<ge> 1/2 + sqrt (6*N/3 - 3)" using c1_def using ceiling_le_iff by blast
   hence b1ngreater:"b1n \<ge> 1/2 + sqrt (6*N/3 - 3)" using b1n_def by simp
   hence b2ngreater:"b2n \<ge> 1/2 + sqrt (6*N/3 - 3)" using bproperties b1n_def b2n_def by linarith
   hence b_ineq1:"b \<ge> 1/2 + sqrt (6*N/3 - 3)" using b_r b1ngreater by auto
 
   have "b2 \<le> c4" using bproperties c1_def c2_def c3_def c4_def by fastforce
   hence "b2 \<le> (2/3 + sqrt (8*N/3 - 8))"
     using \<open>real_of_int c4 < 2 / 3 + sqrt (real (8 * N) / 3 - 8)\<close> by linarith
   hence b2nsmaller:"b2n \<le> (2/3 + sqrt (8*N/3 - 8))" using b2n_def by (metis \<open>int b2n = b2\<close> of_int_of_nat_eq)
   hence "b1n \<le> (2/3 + sqrt (8*N/3 - 8))" using b1n_def bproperties using \<open>int b2n = b2\<close> by linarith
   hence b_ineq2:"b\<le>(2/3 + sqrt (8*N/3 - 8))" using b_r b2nsmaller by auto
-  
+
   define Nr where "Nr = real_of_nat N"
   define ar where "ar = real_of_int a"
   define br where "br = real_of_int b"
   define rr where "rr = real_of_nat r"
   define m where "m = real_of_nat 3"
   from assms have "N\<ge>2*m" using m_def by simp
   then have "Nr \<ge> 2*m" using Nr_def  \<open>N \<ge> 2 * m\<close> by auto
   moreover have "br\<ge>0" using br_def bpos by auto
   moreover have "ar\<ge>0" using ar_def apos by auto
   moreover have "rr\<ge>0" using rr_def b_r by auto
   moreover have "m\<ge>3" using m_def by auto
   moreover have "m>rr" using m_def rr_def b_r by auto
   moreover have "Nr = m*(ar-br)/2+br+rr" using Nr_def ar_def br_def N_expr rr_def m_def \<open>a\<ge>b\<close> by auto
   moreover have "1/2+sqrt(6*Nr/m-3)\<le>br \<and> br\<le>2/3+sqrt(8*Nr/m-8)" using Nr_def  br_def b_ineq1 b_ineq2 m_def by auto
   ultimately have "br^2<4*ar \<and> 3*ar<br^2+2*br+4" using Cauchy_lemma by auto
-  hence real_ineq:"(real_of_int b)^2 < 4*(real_of_int a) \<and> 3*(real_of_int a) < (real_of_int b)^2 + 2*(real_of_int b) + 4" 
+  hence real_ineq:"(real_of_int b)^2 < 4*(real_of_int a) \<and> 3*(real_of_int a) < (real_of_int b)^2 + 2*(real_of_int b) + 4"
     using br_def ar_def by auto
-  hence nat_ineq1: "b^2<4*a" using br_def  by (smt (verit, del_insts) Num.of_nat_simps(4) 
+  hence nat_ineq1: "b^2<4*a" using br_def  by (smt (verit, del_insts) Num.of_nat_simps(4)
 mult.commute mult_2_right nat_distrib(1) numeral_Bit0 of_int_of_nat_eq of_nat_less_of_nat_power_cancel_iff)
   from real_ineq have nat_ineq2: "3*a<b^2+2*b+4" using ar_def br_def of_nat_less_iff by fastforce
 
   obtain s t u v where stuv:"s \<ge> 0 \<and> t \<ge> 0 \<and> u \<ge> 0 \<and> v \<ge> 0 \<and> int a = s^2 + t^2 + u^2 + v^2 \<and>
  int b = s+t+u+v" using apos bpos aodd bodd nat_ineq1 nat_ineq2 four_nonneg_int_sum by presburger
   have a_expr:"a = s^2 + t^2 + u^2 + v^2" using apos stuv by linarith
   have b_expr:"b = s+t+u+v" using bpos stuv by linarith
 
   have "N = r + (s+t+u+v)+ 3*(a-(s+t+u+v))/2" using b_expr N_expr
     by (metis Num.of_nat_simps(4) Num.of_nat_simps(5) \<open>b \<le> a\<close> of_int_of_nat_eq of_nat_diff of_nat_numeral)
   hence "N = 3/2*(s^2-s+t^2-t+u^2-u+v^2-v)+r+(s+t+u+v)" using a_expr by simp
   hence N_expr2:"N = 3/2*(s^2-s)+ 3/2*(t^2-t)+ 3/2*(u^2-u)+ 3/2*(v^2-v)+ r+(s+t+u+v)"
     by (metis (no_types, opaque_lifting) add_diff_eq nat_distrib(2) of_int_add)
 
   have s_div2:"3/2*(s^2-s) = 3*(s^2-s) div 2" using real_of_int_div by auto
   have t_div2:"3/2*(t^2-t) = 3*(t^2-t) div 2" using real_of_int_div by auto
   have u_div2:"3/2*(u^2-u) = 3*(u^2-u) div 2" using real_of_int_div by auto
   have v_div2:"3/2*(v^2-v) = 3*(v^2-v) div 2" using real_of_int_div by auto
   have N_expr3:"N = (3*(s^2-s) div 2+s)+(3*(t^2-t) div 2+t)+(3*(u^2-u) div 2+u)+(3*(v^2-v) div 2+v)+r"
     using N_expr2 s_div2 t_div2 u_div2 v_div2 by simp
 
   define sn where "sn = nat s"
   define tn where "tn = nat t"
   define un where "un = nat u"
   define vn where "vn = nat v"
-  have seqsn:"s^2-s = sn^2 - sn" using stuv sn_def 
+  have seqsn:"s^2-s = sn^2 - sn" using stuv sn_def
     by (metis int_nat_eq le_refl of_nat_diff of_nat_power power2_nat_le_imp_le)
   have teqtn:"t^2-t = tn^2 - tn" using stuv tn_def
     by (metis int_nat_eq le_refl of_nat_diff of_nat_power power2_nat_le_imp_le)
-  have uequn:"u^2-u = un^2 - un" using stuv un_def 
+  have uequn:"u^2-u = un^2 - un" using stuv un_def
     by (metis int_nat_eq le_refl of_nat_diff of_nat_power power2_nat_le_imp_le)
-  have veqvn:"v^2-v = vn^2 - vn" using stuv vn_def 
+  have veqvn:"v^2-v = vn^2 - vn" using stuv vn_def
     by (metis int_nat_eq le_refl of_nat_diff of_nat_power power2_nat_le_imp_le)
 
-  from N_expr3 have 
+  from N_expr3 have
     "N = (3*(sn^2-sn) div 2+s)+(3*(tn^2-tn) div 2+t)+(3*(un^2-un) div 2+u)+(3*(vn^2-vn) div 2+ v)+r"
     using seqsn teqtn uequn veqvn
     by (metis (mono_tags, lifting) Num.of_nat_simps(5) of_nat_numeral zdiv_int)
-  hence "N = (3*(sn^2-sn) div 2+sn)+(3*(tn^2-tn) div 2+tn)+(3*(un^2-un) div 2+un)+(3*(vn^2-vn) div 2+ v)+r" 
+  hence "N = (3*(sn^2-sn) div 2+sn)+(3*(tn^2-tn) div 2+tn)+(3*(un^2-un) div 2+un)+(3*(vn^2-vn) div 2+ v)+r"
     using sn_def tn_def un_def  stuv int_nat_eq int_ops(5) by presburger
   hence "N = (3*(sn^2-sn) div 2+sn)+(3*(tn^2-tn) div 2+tn)+(3*(un^2-un) div 2+un)+(3*(vn^2-vn) div 2+ vn)+r"
     using vn_def stuv by (smt (verit, del_insts) Num.of_nat_simps(4) int_nat_eq of_nat_eq_iff)
   hence "N = (3* sn*(sn-1) div 2+sn)+(3*tn*(tn-1) div 2+tn)+(3*un*(un-1) div 2+un)+(3* vn*(vn-1) div 2+ vn)+r"
     by (smt (verit, ccfv_threshold) more_arith_simps(11) mult.right_neutral power2_eq_square right_diff_distrib')
   hence N_expr4:"N = polygonal_number 3 sn + polygonal_number 3 tn + polygonal_number 3 un + polygonal_number 3 vn +r"
     using Polygonal_Number_Theorem_Gauss.polygonal_number_def by presburger
 
   define p1 where "p1 = polygonal_number 3 sn"
   define p2 where "p2 = polygonal_number 3 tn"
   define p3 where "p3 = polygonal_number 3 un"
   define p4 where "p4 = polygonal_number 3 vn"
   have N_expr5:"N = p1 + p2 + p3 + p4 + r" using N_expr4 p1_def p2_def p3_def p4_def by auto
   thus ?thesis using p1_def p2_def p3_def p4_def b_r by blast
 qed
 end
\ No newline at end of file
diff --git a/thys/Polygonal_Number_Theorem/Polygonal_Number_Theorem_Legendre.thy b/thys/Polygonal_Number_Theorem/Polygonal_Number_Theorem_Legendre.thy
--- a/thys/Polygonal_Number_Theorem/Polygonal_Number_Theorem_Legendre.thy
+++ b/thys/Polygonal_Number_Theorem/Polygonal_Number_Theorem_Legendre.thy
@@ -1,613 +1,613 @@
 subsection \<open> Legendre's Polygonal Number Theorem \<close>
-text\<open>We will use the definition of the polygonal numbers from the Gauss Theorem theory file 
+text\<open>We will use the definition of the polygonal numbers from the Gauss Theorem theory file
 which also imports the Three Squares Theorem AFP entry \cite{Three_Squares-AFP}.\<close>
 
 theory Polygonal_Number_Theorem_Legendre
   imports Polygonal_Number_Theorem_Gauss
 begin
 
 text \<open>This lemma shows that under certain conditions, an integer $N$ can be written as the sum of four polygonal numbers.\<close>
 
 lemma sum_of_four_polygonal_numbers:
   fixes N m :: nat
   fixes b :: int
   assumes "m \<ge> 3"
   assumes "N \<ge> 2*m"
   assumes "[N = b] (mod m)"
   assumes odd_b: "odd b"
   assumes "b \<in> {1/2 + sqrt (6*N/m - 3) .. 2/3 + sqrt (8*N/m - 8)}"
   assumes "N \<ge> 9"
   shows "\<exists>k1 k2 k3 k4. N = polygonal_number m k1 + polygonal_number m k2 + polygonal_number m k3 + polygonal_number m k4"
 
 proof -
   define I where "I = {1/2 + sqrt (6*N/m - 3) .. 2/3 + sqrt (8*N/m - 8)}"
   from assms(5) I_def have "b \<in> I" by auto
   define a::int where a_def: "a = 2*(N-b) div m + b"
   have "m dvd (N-b)" using assms(3)
     by (smt (verit, ccfv_threshold) cong_iff_dvd_diff zdvd_zdiffD)
   hence "even (2*(N-b) div m)"
     by (metis div_mult_swap dvd_triv_left)
-  hence "odd a" using a_def assms(3) odd_b by auto 
+  hence "odd a" using a_def assms(3) odd_b by auto
   from assms(1) have "m^3 \<ge> m"
     by (simp add: power3_eq_cube)
   hence "N \<ge> 2 * m" using assms(1,2) by simp
   from assms(1) have m_pos: "m > 0" by auto
   have "N \<ge> b"
   proof -
     from assms(1) have "m \<ge> 1" by auto
     hence "1/m \<le> 1" using m_pos by auto
     moreover have "N > 0" using \<open>N \<ge> 2 * m\<close> m_pos by auto
     ultimately have "N/m \<le> N"
       using divide_less_eq_1 less_eq_real_def by fastforce
     hence "sqrt(8*N/m - 8) \<le> sqrt(8*(N-1))" by auto
     from assms(1) have "m^3 \<ge> 3*3*(3::real)"
       by (metis numeral_le_real_of_nat_iff numeral_times_numeral power3_eq_cube power_mono zero_le_numeral)
     from \<open>N \<ge> 9\<close> have "N-1 \<ge> 8" by auto
     hence "(N-1)^2 \<ge> 8*(N-1)" using \<open>N > 0\<close> by (simp add: power2_eq_square)
     hence "(N-1) \<ge> sqrt (8*(N-1))" using \<open>N > 0\<close>
       by (metis of_nat_0_le_iff of_nat_mono of_nat_power real_sqrt_le_mono real_sqrt_pow2 real_sqrt_power)
     hence "N - (1::real) - sqrt(8*N/m - 8) \<ge> 0"
       using \<open>sqrt (real (8 * N) / real m - 8) \<le> sqrt (real (8 * (N - 1)))\<close> \<open>9 \<le> N\<close> by linarith
     hence expr_pos: "N - (2/3::real) - sqrt(8*N/m - 8) \<ge> 0" by auto
     have "b \<le> 2/3 + sqrt(8*N/m - 8)" using \<open>b \<in> I\<close> I_def by auto
     hence "N - b \<ge> N - (2/3 + sqrt(8*N/m-8))" by auto
     hence "N - b \<ge> 0"
       using expr_pos of_int_0_le_iff by auto
     thus ?thesis by auto
   qed
   from \<open>N \<ge> 2 * m\<close> m_pos have "6*N/m - 3 \<ge> 0" by (simp add: mult_imp_le_div_pos)
   hence "1/2 + sqrt (6*N/m - 3) > 0"
-    by (smt (verit, del_insts) divide_le_0_1_iff real_sqrt_ge_zero) 
+    by (smt (verit, del_insts) divide_le_0_1_iff real_sqrt_ge_zero)
   with \<open>b \<in> I\<close> assms(3) I_def have "b \<ge> 1" by auto
   hence b_pos: "b \<ge> 0" by auto
   from \<open>b \<in> I\<close> have b_in_I: "(1/2::real) + sqrt (6* real N / real m - 3) \<le> b \<and> b \<le> (2/3::real) + sqrt (8 * real N/real m - 8)" unfolding I_def by auto
   from b_pos \<open>N \<ge> b\<close> a_def have a_pos: "a \<ge> 0"
     by (smt (verit) m_pos of_nat_0_less_iff pos_imp_zdiv_neg_iff)
   hence "a \<ge> 1"
     by (smt (verit) \<open>odd a\<close> dvd_0_right)
   have "a - b = 2*(N-b) div m" using a_def by auto
   from \<open>int m dvd (int N - b)\<close> have "m dvd 2*(N-b)" by fastforce
   have "a = 2*(N-b)/m + b" using a_def m_pos
     using \<open>int m dvd 2 * (int N - b)\<close> by fastforce
   hence "a = 2*N/m - 2*b/m + b"
     by (simp add: assms diff_divide_distrib of_nat_diff)
   hence "(2::real)*N/m = a + 2*b/m - b" by auto
   hence "(2::real)*N = (a + 2*b/m - b)*m"
     using m_pos by (simp add: divide_eq_eq)
   hence "(2::real)*N = m*(a-b) + 2*b"
     using \<open>int m dvd 2 * (int N - b)\<close> a_def by auto
   hence "N = m*(a-b)/2 + b" by auto
   hence N_expr: "real N = real m * (of_int a - of_int b) / 2 + of_int b" by auto
   have "even (a-b)" using \<open>odd a\<close> \<open>odd b\<close> by auto
   hence "2 dvd m*(a-b)" by auto
   hence N_expr2: "N = m*(a-b) div 2 + b" using \<open>N = m*(a-b)/2 + b\<close> by linarith
   define Nr where "Nr = real_of_nat N"
   define mr where "mr = real m"
   define ar where "ar = real_of_int a"
   define br where "br = real_of_int b"
   from assms(1) have "mr \<ge> 3" using mr_def by auto
   moreover have "Nr \<ge> 2*mr" using Nr_def mr_def \<open>N \<ge> 2 * m\<close> by auto
   moreover have "br \<ge> 0" using br_def b_pos by auto
   moreover have "mr > 0" using mr_def m_pos by auto
   moreover have "ar \<ge> 0" using ar_def \<open>a \<ge> 0\<close> by auto
   moreover have "Nr = mr*(ar-br)/2 + br" using Nr_def mr_def ar_def br_def N_expr by auto
   moreover have "1/2 + sqrt (6*Nr/mr-3) \<le> br \<and> br \<le> 2/3 + sqrt (8*Nr/mr-8)" using Nr_def mr_def br_def b_in_I by auto
   ultimately have "br^2 < 4*ar \<and> 3*ar < br^2+2*br+4" using Cauchy_lemma_r_eq_zero
     by auto
-  hence real_ineq:"(real_of_int b)^2 < 4*(real_of_int a) \<and> 3*(real_of_int a) < (real_of_int b)^2 + 2*(real_of_int b) + 4" 
+  hence real_ineq:"(real_of_int b)^2 < 4*(real_of_int a) \<and> 3*(real_of_int a) < (real_of_int b)^2 + 2*(real_of_int b) + 4"
     using br_def ar_def by auto
   hence int_ineq1: "b^2<4*a" using of_int_less_iff by fastforce
   from real_ineq have int_ineq2: "3*a < b^2+2*b+4" using of_int_less_iff by fastforce
 
   define an:: nat where "an = nat a"
   from a_pos have "an = a" unfolding an_def by auto
   define bn:: nat where "bn = nat b"
   from b_pos have "bn = b" unfolding bn_def by auto
   have "an \<ge> 1" using \<open>int an = a\<close> \<open>a \<ge> 1\<close> by auto
   moreover have "bn \<ge> 1" using \<open>int bn = b\<close> \<open>b \<ge> 1\<close> by auto
   moreover have "odd an" using \<open>odd a\<close> \<open>int an = a\<close> by auto
   moreover have "odd bn" using \<open>odd b\<close> \<open>int bn = b\<close> by auto
   moreover have "bn ^ 2 < 4 * an" using int_ineq1 \<open>int an = a\<close> \<open>int bn = b\<close>
     using of_nat_less_iff by fastforce
   moreover have "3 * an < bn ^ 2 + 2 * bn + 4" using int_ineq2 \<open>int an = a\<close> \<open>int bn = b\<close>
     using of_nat_less_iff by fastforce
   ultimately have "\<exists>s t u v :: int. s \<ge> 0 \<and> t \<ge> 0 \<and> u \<ge> 0 \<and> v \<ge> 0 \<and> an = s^2 + t^2 + u^2 + v^2 \<and>
 bn = s+t+u+v" using four_nonneg_int_sum by auto
   hence "\<exists>s t u v :: int. s \<ge> 0 \<and> t \<ge> 0 \<and> u \<ge> 0 \<and> v \<ge> 0 \<and> a = s^2 + t^2 + u^2 + v^2 \<and>
 b = s+t+u+v" using \<open>int an = a\<close> \<open>int bn = b\<close> by auto
   then obtain s t u v :: int where stuv: "s \<ge> 0 \<and> t \<ge> 0 \<and> u \<ge> 0 \<and> v \<ge> 0 \<and> a = s^2 + t^2 + u^2 + v^2 \<and>
 b = s+t+u+v" by auto
   hence "N = (m*(s^2+t^2+u^2+v^2-s-t-u-v) div 2) + s+t+u+v" using N_expr2 by (smt (verit, ccfv_threshold))
   hence "N = (m*(s^2-s+t^2-t+u^2-u+v^2-v) div 2) + s+t+u+v" by (smt (verit, ccfv_SIG))
   hence "N = (m * (s * (s-1) + t * (t-1) + u * (u-1) + v * (v-1)) div 2) +s+t+u+v" by (simp add: power2_eq_square algebra_simps)
   hence previous_step: "N = (m * s * (s-1) + m * t * (t-1) + m * u * (u-1) + m * v * (v-1)) div 2 + s+t+u+v" by (simp add: algebra_simps)
   moreover have "2 dvd m * s * (s-1)" by simp
   moreover have "2 dvd m * t * (t-1)" by simp
   moreover have "2 dvd m * u * (u-1)" by simp
   moreover have "2 dvd m * v * (v-1)" by simp
   ultimately have "N = m * s * (s-1) div 2 + m * t * (t-1) div 2 + m * u * (u-1) div 2 + m * v *(v-1) div 2 + s+t+u+v" by fastforce
   hence N_expr3: "N = m * s * (s-1) div 2 + s + m * t * (t-1) div 2 + t + m * u * (u-1) div 2 + u + m * v * (v-1) div 2 + v" by auto
   define sn::nat where "sn = nat s"
   define tn::nat where "tn = nat t"
   define un::nat where "un = nat u"
   define vn::nat where "vn = nat v"
   have "sn = s" using stuv sn_def by auto
   hence "m * sn * (sn-1) = m * s * (s-1)" by fastforce
   hence "m * sn * (sn-1) div 2 = m * s * (s-1) div 2" by linarith
   have "tn = t" using stuv tn_def by auto
   hence "m * tn * (tn-1) = m * t * (t-1)" by fastforce
   hence "m * tn * (tn-1) div 2 = m * t * (t-1) div 2" by linarith
   have "un = u" using stuv un_def by auto
   hence "m * un * (un-1) = m * u * (u-1)" by fastforce
   hence "m * un * (un-1) div 2 = m * u * (u-1) div 2" by linarith
   have "vn = v" using stuv vn_def by auto
   hence "m * vn * (vn-1) = m * v * (v-1)" by fastforce
   hence "m * vn * (vn-1) div 2 = m * v * (v-1) div 2" by linarith
   have "N = m * sn * (sn-1) div 2 + sn + m * tn * (tn-1) div 2 + tn + m * un * (un-1) div 2 + un + m * vn * (vn-1) div 2 + vn"
     using N_expr3 \<open>sn = s\<close> \<open>tn = t\<close> \<open>un = u\<close> \<open>vn = v\<close> \<open>m * sn * (sn-1) div 2 = m * s * (s-1) div 2\<close> \<open>m * tn * (tn-1) div 2 = m * t * (t-1) div 2\<close> \<open>m * un * (un-1) div 2 = m * u * (u-1) div 2\<close> \<open>m * vn * (vn-1) div 2 = m * v * (v-1) div 2\<close> by linarith
   hence "N = polygonal_number m sn + polygonal_number m tn + polygonal_number m un + polygonal_number m vn"
     using Polygonal_Number_Theorem_Gauss.polygonal_number_def by presburger
   thus ?thesis by blast
 qed
 
 text \<open>We show Legendre's polygonal number theorem which corresponds to Theorem 1.10 in \cite{nathanson1996}.\<close>
 
 theorem Legendre_Polygonal_Number_Theorem:
   fixes m N :: nat
   assumes "m \<ge> 3"
   assumes "N \<ge> 28*m^3"
   shows "odd m \<Longrightarrow> \<exists>k1 k2 k3 k4::nat. N = polygonal_number m k1 + polygonal_number m k2 + polygonal_number m k3 + polygonal_number m k4"
 and "even m \<Longrightarrow> \<exists>k1 k2 k3 k4 k5::nat. N = polygonal_number m k1 + polygonal_number m k2 + polygonal_number m k3 + polygonal_number m k4 + polygonal_number m k5 \<and> (k1 = 0 \<or> k1 = 1 \<or> k2 = 0 \<or> k2 = 1 \<or> k3 = 0 \<or> k3 = 1 \<or> k4 = 0 \<or> k4 = 1 \<or> k5 = 0 \<or> k5 = 1)"
 
 proof -
   define L :: real where "L = (2/3 + sqrt (8*N/m - 8)) - (1/2 + sqrt (6*N/m - 3))"
   define I where "I = {1/2 + sqrt (6*N/m - 3) .. 2/3 + sqrt (8*N/m - 8)}"
   from assms(1) have "m^3 \<ge> m"
     by (simp add: power3_eq_cube)
   hence "N \<ge> 2 * m" using assms by simp
   have m_pos: "m > 0" using assms(1) by simp
   have "L > 2 * of_nat m" using assms \<open>N \<ge> 2 * m\<close> m_pos L_def
     apply -
     apply (rule interval_length_greater_than_2m[where N="of_nat N" and m="of_nat m"])
        apply (simp_all)
     by (metis (no_types, opaque_lifting) of_nat_le_iff of_nat_mult of_nat_numeral power3_eq_cube)
   hence 2: "L > 2 * m" by simp
   show thm_odd_m: "odd m \<Longrightarrow> \<exists>k1 k2 k3 k4. N = polygonal_number m k1 + polygonal_number m k2 + polygonal_number m k3 + polygonal_number m k4"
   proof -
     assume odd_m: "odd m"
     from assms(1) have "m > 0" by auto
     define ce where "ce = \<lceil>1/2 + sqrt (6*N/m - 3)\<rceil>"
     have "\<forall> i\<in>{0..2*m-1}. ce + i \<ge> ce" by auto
     hence lower_bound: "\<forall> i\<in>{0..2*m-1}. ce + i \<ge> 1/2 + sqrt (6*N/m - 3)" using ceiling_le_iff ce_def by blast
     have "2*m-1 + ce \<le> 2/3 + sqrt (8*N/m - 8)" using 2 L_def assms(1) ce_def by linarith
     hence upper_bound: "\<forall> i\<in>{0..2*m-1}. ce + i \<le>  2/3 + sqrt (8*N/m - 8)" by auto
     from lower_bound upper_bound have in_interval: "\<forall> i\<in>{0..2*m-1}. ce + i \<in> I" unfolding ce_def I_def by auto
     have "\<exists> f::nat \<Rightarrow> int. (\<forall> i\<in>{0..m-1}. odd (f i)) \<and> (\<forall> i\<in>{1..m-1}. f i = f 0 + 2*i) \<and> (\<forall> i\<in>{0..m-1}. f i \<in> I)"
     proof -
       have ?thesis if odd_f0: "odd ce"
       proof -
         define g::"nat \<Rightarrow> int" where "g i = ce + 2*i"
         have "odd (g 0)" using odd_f0 \<open>g \<equiv> \<lambda>i. ce + int (2 * i)\<close> by auto
         hence "\<forall> i\<in>{0..m-1}. odd (g i)" using \<open>g \<equiv> \<lambda>i. ce + int (2 * i)\<close> by auto
         have "\<forall> i\<in>{1..m-1}. g i = g 0 + 2*i" using \<open>g \<equiv> \<lambda>i. ce + int (2 * i)\<close> by auto
         have "\<forall> i\<in>{0..m-1}. 2*i < 2*m-1" using m_pos by auto
         hence "\<forall> i\<in>{0..m-1}. g i \<in> I" using \<open>g \<equiv> \<lambda>i. ce + int (2 * i)\<close> in_interval by fastforce
         show ?thesis using \<open>\<forall>i\<in>{0..m - 1}. odd (g i)\<close> \<open>\<forall>i\<in>{0..m - 1}. real_of_int (g i) \<in> I\<close> \<open>\<forall>i\<in>{1..m - 1}. g i = g 0 + int(2 * i)\<close> by blast
       qed
       moreover have ?thesis if "even ce"
       proof -
         from \<open>even ce\<close> have odd_f1: "odd (ce + 1)" by auto
         define g::"nat \<Rightarrow> int" where "g i = ce + (2*i + 1)"
         have "odd (g 0)" using odd_f1 \<open>g \<equiv> \<lambda>i. ce + int (2 * i + 1)\<close> by auto
         hence "\<forall> i\<in>{0..m-1}. odd (g i)" using \<open>g \<equiv> \<lambda>i. ce + int (2 * i + 1)\<close> by auto
         have "\<forall> i\<in>{1..m-1}. g i = g 0 + 2*i" using \<open>g \<equiv> \<lambda>i. ce + int (2 * i + 1)\<close> by auto
         have "\<forall> i\<in>{0..m-1}. 2*i + 1 \<le> 2*m-1" using m_pos by auto
         hence "\<forall> i\<in>{0..m-1}. g i \<in> I" using \<open>g \<equiv> \<lambda>i. ce + int (2 * i + 1)\<close> in_interval by fastforce
         show ?thesis using \<open>\<forall>i\<in>{0..m - 1}. odd (g i)\<close> \<open>\<forall>i\<in>{0..m - 1}. real_of_int (g i) \<in> I\<close> \<open>\<forall>i\<in>{1..m - 1}. g i = g 0 + int(2 *i)\<close> by blast
       qed
       ultimately show ?thesis by blast
     qed
     then obtain f::"nat \<Rightarrow> int" where f_def: "(\<forall> i\<in>{0..m-1}. odd (f i)) \<and> (\<forall> i\<in>{1..m-1}. f i = f 0 + 2*i) \<and> (\<forall> i\<in>{0..m-1}. f i \<in> I)" by auto
-    
+
     have inj_lemma: "\<lbrakk>i \<in> {0..m-1}; j \<in> {0..m-1}; [f i = f j] (mod m)\<rbrakk> \<Longrightarrow> i = j" for i j
     proof -
       assume asm1: "i \<in> {0..m-1}"
       assume asm2: "j \<in> {0..m-1}"
       assume asm3: "[f i = f j] (mod m)"
       from f_def have "odd (f 0)" by auto
       hence "\<exists> k::int. f 0 = 2*k + 1" by (metis oddE)
       then obtain k::int where k_def: "f 0 = 2*k + 1" by auto
       have False if case2: "i = 0 \<and> j > 0"
       proof -
         have "f j = f 0 + 2*j" using f_def case2 asm2 by auto
         hence "[2*k + 1 = 2*k + 1 + 2*j] (mod m)" using asm3 case2 k_def by auto
         hence "[2*j = 0] (mod m)"
           by (metis cong_add_lcancel_0 cong_int_iff cong_sym_eq int_ops(1))
         have "coprime 2 m" using odd_m by simp
         hence "[j = 0] (mod m)" using \<open>[2*j = 0] (mod m)\<close> by (simp add: cong_0_iff coprime_dvd_mult_right_iff)
         thus False using asm2 case2 cong_less_modulus_unique_nat by fastforce
       qed
       moreover have False if case3: "i > 0 \<and> j = 0"
       proof -
         have "f i = f 0 + 2*i" using f_def case3 asm1 by auto
         hence "[2*k + 1 + 2*i = 2*k + 1] (mod m)" using asm3 case3 k_def by auto
         hence "[2*i = 0] (mod m)"
           by (metis cong_add_lcancel_0 cong_int_iff cong_sym_eq int_ops(1))
         have "coprime 2 m" using odd_m by simp
         hence "[i = 0] (mod m)" using \<open>[2*i = 0] (mod m)\<close> by (simp add: cong_0_iff coprime_dvd_mult_right_iff)
         thus False using asm1 case3 cong_less_modulus_unique_nat by fastforce
       qed
       moreover have ?thesis if case4: "i > 0 \<and> j > 0"
       proof -
         have "i > 0" and "j > 0" using case4 by auto
         have "f i = f 0 + 2*i" using f_def case4 asm1 by auto
         moreover have "f j = f 0 + 2*j" using f_def case4 asm2 by auto
         ultimately have "[2*k + 1 + 2*i = 2*k + 1 + 2*j] (mod m)" using case4 k_def asm3 by fastforce
         hence "[2*i = 2*j] (mod m)"
           using cong_add_lcancel cong_int_iff by blast
         have "coprime 2 m" using odd_m by simp
         hence "[i = j] (mod m)"
           using \<open>[2 * i = 2 * j] (mod m)\<close> cong_mult_lcancel_nat by auto
         thus ?thesis using asm1 asm2 case4 cong_less_modulus_unique_nat by auto
       qed
       ultimately show ?thesis by fastforce
     qed
     have complete_cong_class: "\<exists>i \<in> {0..m-1}. [f i = S] (mod m)" for S
     proof -
       have "(f i) mod m = (f j) mod m \<Longrightarrow> [f i = f j] (mod m)" for i j
         by (simp add: unique_euclidean_semiring_class.cong_def)
       hence inj2: "\<lbrakk>i \<in> {0..m-1}; j \<in> {0..m-1}; (f i) mod m = (f j) mod m\<rbrakk> \<Longrightarrow> i = j" for i j
         using inj_lemma by auto
       hence injective: "\<forall>i \<in> {0..m-1}. \<forall>j \<in> {0..m-1}. (f i) mod m = (f j) mod m \<longrightarrow> i = j"
         by auto
       define g :: "nat \<Rightarrow> int" where "g i = (f i) mod m"
       then have g_inj2: "\<forall>i \<in> {0..m-1}. \<forall> j \<in> {0..m-1}. g i = g j \<longrightarrow> i = j"
         using \<open>g \<equiv> \<lambda>i. f i mod int m\<close> injective  by fastforce
       then have g_inj: "inj_on g {0..m-1}"
         by (meson inj_onI)
       have g_range2: "\<forall> i \<in> {0..m-1}. g i \<in> {0..m-1}" using \<open>g \<equiv> \<lambda>i. f i mod int m\<close>
-        by (metis m_pos Euclidean_Division.pos_mod_bound Euclidean_Division.pos_mod_sign atLeastAtMost_iff mod_by_1 mod_if not_gr0 of_nat_0_less_iff of_nat_1 of_nat_diff verit_comp_simplify1(3) zle_diff1_eq)
+        by (metis m_pos Euclidean_Rings.pos_mod_bound Euclidean_Rings.pos_mod_sign atLeastAtMost_iff mod_by_1 mod_if not_gr0 of_nat_0_less_iff of_nat_1 of_nat_diff verit_comp_simplify1(3) zle_diff1_eq)
       hence image_subset: "g ` {0..m-1} \<subseteq> {0..m-1}" by blast
       have g_range: "i \<in> {0..m-1} \<Longrightarrow> g i \<in> {0..m-1}" using \<open>g \<equiv> \<lambda>i. f i mod int m\<close>
-        by (metis m_pos Euclidean_Division.pos_mod_bound Euclidean_Division.pos_mod_sign atLeastAtMost_iff mod_by_1 mod_if not_gr0 of_nat_0_less_iff of_nat_1 of_nat_diff verit_comp_simplify1(3) zle_diff1_eq)
+        by (metis m_pos Euclidean_Rings.pos_mod_bound Euclidean_Rings.pos_mod_sign atLeastAtMost_iff mod_by_1 mod_if not_gr0 of_nat_0_less_iff of_nat_1 of_nat_diff verit_comp_simplify1(3) zle_diff1_eq)
       have card_ge_m: "card (g ` {0..m-1}) \<ge> m" using g_inj
         by (metis m_pos Suc_diff_1 card_atLeastAtMost card_image minus_nat.diff_0 verit_comp_simplify1(2))
       have "card {0..m-1} = m" using m_pos by force
       hence card_le_m: "card (g ` {0..m-1}) \<le> m" using m_pos
         by (metis card_image g_inj le_refl)
       from card_ge_m card_le_m have image_size: "card (g ` {0..m-1}) = m" by auto
       with \<open>card {0..m-1} = m\<close> have equal_card: "card (g ` {0..m-1}) = card {0..m-1}" by auto
       have "finite (g ` {0..m-1})" using image_size by auto
       with equal_card image_subset have "g ` {0..m-1} = {0..m-1}"
         by (metis card_image card_subset_eq finite_atLeastAtMost_int image_int_atLeastAtMost inj_on_of_nat of_nat_0)
       hence "i \<in> {0..m-1} \<Longrightarrow> \<exists> j \<in> {0..m-1}. i = g j" for i by auto
       hence "i \<in> {0..m-1} \<Longrightarrow> \<exists> j \<in> {0..m-1}. i = (f j) mod m" for i
-        using \<open>g \<equiv> \<lambda>i. f i mod int m\<close> by auto  
+        using \<open>g \<equiv> \<lambda>i. f i mod int m\<close> by auto
       hence surj: "i \<in> {0..m-1} \<Longrightarrow> \<exists> j \<in> {0..m-1}. [i = f j] (mod m)" for i
         by (metis mod_mod_trivial unique_euclidean_semiring_class.cong_def)
       have "S mod m \<ge> 0" using m_pos by simp
       moreover have "S mod m \<le> m-1"
         using m_pos by (simp add: of_nat_diff)
       ultimately have "S mod m \<in> {0..m-1}" by auto
       with surj m_pos have "\<exists> j \<in> {0..m-1}. [S mod m = f j] (mod m)"
         by (metis atLeastAtMost_iff less_eq_nat.simps(1) nonneg_int_cases of_nat_less_iff verit_comp_simplify(3))
       thus ?thesis using cong_mod_right cong_sym by blast
     qed
     have "\<exists> b::int. [N = b] (mod m) \<and> odd b \<and> b \<in> I"
     proof -
       have "N mod m \<ge> 0" by auto
       moreover have "N mod m \<le> m-1"
         using m_pos less_Suc_eq_le by fastforce
       ultimately have "N mod m \<in> {0..m-1}" by auto
       with complete_cong_class have "\<exists> i. i \<in> {0..m-1} \<and> [f i = N] (mod m)" by blast
       then obtain c::nat where c_def: "c \<in> {0..m-1} \<and> [f c = N] (mod m)" by auto
       define b::int where "b = f c"
       have "[N = b] (mod m)" using b_def c_def by (metis cong_sym)
       moreover have "odd b" using b_def f_def c_def by auto
       moreover have "b \<in> I" using b_def f_def c_def by auto
       ultimately show ?thesis by auto
     qed
     then obtain b::int where b_def: "[N = b] (mod m) \<and> odd b \<and> b \<in> I" by auto
     have "m^3 \<ge> m" using m_pos by (auto simp add: power3_eq_cube)
     hence "N \<ge> 28*m" using assms(1,2) by linarith
     hence "N \<ge> 2*m" by simp
     have "m^3 \<ge> 3*3*(3::nat)" using assms(1)
       by (metis power3_eq_cube power_mono zero_le_numeral)
     hence "N \<ge> 28*3*3*(3::nat)" using assms(2) by auto
     hence "N \<ge> 9" by simp
     show ?thesis using sum_of_four_polygonal_numbers assms(1) b_def I_def \<open>N \<ge> 2 * m\<close> \<open>N \<ge> 9\<close> by blast
   qed
   show thm_even_m: "even m \<Longrightarrow> \<exists>k1 k2 k3 k4 k5. N = polygonal_number m k1 + polygonal_number m k2 + polygonal_number m k3 + polygonal_number m k4 + polygonal_number m k5 \<and> (k1 = 0 \<or> k1 = 1 \<or> k2 = 0 \<or> k2 = 1 \<or> k3 = 0 \<or> k3 = 1 \<or> k4 = 0 \<or> k4 = 1 \<or> k5 = 0 \<or> k5 = 1)"
   proof -
     assume even_m: "even m"
     from assms(1) have "m > 0" by auto
     define ce where "ce = \<lceil>1/2 + sqrt (6*N/m - 3)\<rceil>"
     have "\<forall> i\<in>{0..m-1}. ce + i \<ge> ce" by auto
     hence lower_bound: "\<forall> i\<in>{0..m-1}. ce + i \<ge> 1/2 + sqrt (6*N/m - 3)" using ceiling_le_iff ce_def by blast
     have "m-1 + ce \<le> 2/3 + sqrt (8*N/m - 8)" using 2 L_def assms(1) ce_def by linarith
     hence upper_bound: "\<forall> i\<in>{0..m-1}. ce + i \<le>  2/3 + sqrt (8*N/m - 8)" by auto
     from lower_bound upper_bound have in_interval: "\<forall> i\<in>{0..m-1}. ce + i \<in> I" unfolding ce_def I_def by auto
     have "\<exists> f::nat \<Rightarrow> int. (\<forall> i\<in>{1..m-1}. f i = f 0 + i) \<and> (\<forall> i\<in>{0..m-1}. f i \<in> I)"
     proof -
       define g::"nat \<Rightarrow> int" where "g i = ce + i"
       have "\<forall> i\<in>{1..m-1}. g i = g 0 + i" using \<open>g \<equiv> \<lambda>i. ce + int i\<close> by auto
       have "\<forall> i\<in>{0..m-1}. i < m" using m_pos by auto
       hence "\<forall> i\<in>{0..m-1}. g i \<in> I" using \<open>g \<equiv> \<lambda>i. ce + int i\<close> in_interval by fastforce
       show ?thesis by (metis Num.of_nat_simps(1) \<open>\<forall>i\<in>{0..m - 1}. real_of_int (g i) \<in> I\<close> \<open>g \<equiv> \<lambda>i. ce + int i\<close> arith_extra_simps(6))
     qed
     then obtain f::"nat \<Rightarrow> int" where f_def: "(\<forall> i\<in>{1..m-1}. f i = f 0 + i) \<and> (\<forall> i\<in>{0..m-1}. f i \<in> I)" by auto
     have inj_lemma: "\<lbrakk>i \<in> {0..m-1}; j \<in> {0..m-1}; [f i = f j] (mod m)\<rbrakk> \<Longrightarrow> i = j" for i j
     proof -
       assume asm1: "i \<in> {0..m-1}"
       assume asm2: "j \<in> {0..m-1}"
       assume asm3: "[f i = f j] (mod m)"
       have False if case2: "i = 0 \<and> j > 0"
       proof -
         have "f j = f 0 + j" using f_def case2 asm2 by auto
         hence "[f 0  = f 0 + j] (mod m)" using asm3 case2 by auto
         hence "[j = 0] (mod m)"
           by (metis cong_add_lcancel_0 cong_int_iff cong_sym_eq int_ops(1))
         thus False using asm2 case2 cong_less_modulus_unique_nat by fastforce
       qed
       moreover have False if case3: "i > 0 \<and> j = 0"
       proof -
         have "f i = f 0 + i" using f_def case3 asm1 by auto
         hence "[f 0 + i = f 0] (mod m)" using asm3 case3 by auto
         hence "[i = 0] (mod m)"
           by (metis cong_add_lcancel_0 cong_int_iff cong_sym_eq int_ops(1))
         thus False using asm1 case3 cong_less_modulus_unique_nat by fastforce
       qed
       moreover have ?thesis if case4: "i > 0 \<and> j > 0"
       proof -
         have "i > 0" and "j > 0" using case4 by auto
         have "f i = f 0 + i" using f_def case4 asm1 by auto
         moreover have "f j = f 0 + j" using f_def case4 asm2 by auto
         ultimately have "[f 0 + i = f 0 + j] (mod m)" using case4 asm3 by fastforce
         hence "[i = j] (mod m)"
           using cong_add_lcancel cong_int_iff by blast
         thus ?thesis using asm1 asm2 case4 cong_less_modulus_unique_nat by auto
       qed
       ultimately show ?thesis by fastforce
     qed
     have complete_cong_class: "\<exists>i \<in> {0..m-1}. [f i = S] (mod m)" for S
     proof -
       have "(f i) mod m = (f j) mod m \<Longrightarrow> [f i = f j] (mod m)" for i j
         by (simp add: unique_euclidean_semiring_class.cong_def)
       hence inj2: "\<lbrakk>i \<in> {0..m-1}; j \<in> {0..m-1}; (f i) mod m = (f j) mod m\<rbrakk> \<Longrightarrow> i = j" for i j
         using inj_lemma by auto
       hence injective: "\<forall>i \<in> {0..m-1}. \<forall>j \<in> {0..m-1}. (f i) mod m = (f j) mod m \<longrightarrow> i = j"
         by auto
       define g :: "nat \<Rightarrow> int" where "g i = (f i) mod m"
       then have g_inj2: "\<forall>i \<in> {0..m-1}. \<forall> j \<in> {0..m-1}. g i = g j \<longrightarrow> i = j"
         using \<open>g \<equiv> \<lambda>i. f i mod int m\<close> injective  by fastforce
       then have g_inj: "inj_on g {0..m-1}"
         by (meson inj_onI)
       have g_range2: "\<forall> i \<in> {0..m-1}. g i \<in> {0..m-1}" using \<open>g \<equiv> \<lambda>i. f i mod int m\<close>
-        by (metis m_pos Euclidean_Division.pos_mod_bound Euclidean_Division.pos_mod_sign atLeastAtMost_iff mod_by_1 mod_if not_gr0 of_nat_0_less_iff of_nat_1 of_nat_diff verit_comp_simplify1(3) zle_diff1_eq)
+        by (metis m_pos Euclidean_Rings.pos_mod_bound Euclidean_Rings.pos_mod_sign atLeastAtMost_iff mod_by_1 mod_if not_gr0 of_nat_0_less_iff of_nat_1 of_nat_diff verit_comp_simplify1(3) zle_diff1_eq)
       hence image_subset: "g ` {0..m-1} \<subseteq> {0..m-1}" by blast
       have g_range: "i \<in> {0..m-1} \<Longrightarrow> g i \<in> {0..m-1}" using \<open>g \<equiv> \<lambda>i. f i mod int m\<close>
-        by (metis m_pos Euclidean_Division.pos_mod_bound Euclidean_Division.pos_mod_sign atLeastAtMost_iff mod_by_1 mod_if not_gr0 of_nat_0_less_iff of_nat_1 of_nat_diff verit_comp_simplify1(3) zle_diff1_eq)
+        by (metis m_pos Euclidean_Rings.pos_mod_bound Euclidean_Rings.pos_mod_sign atLeastAtMost_iff mod_by_1 mod_if not_gr0 of_nat_0_less_iff of_nat_1 of_nat_diff verit_comp_simplify1(3) zle_diff1_eq)
       have card_ge_m: "card (g ` {0..m-1}) \<ge> m" using g_inj
         by (metis m_pos Suc_diff_1 card_atLeastAtMost card_image minus_nat.diff_0 verit_comp_simplify1(2))
       have "card {0..m-1} = m" using m_pos by force
       hence card_le_m: "card (g ` {0..m-1}) \<le> m" using m_pos
         by (metis card_image g_inj le_refl)
       from card_ge_m card_le_m have image_size: "card (g ` {0..m-1}) = m" by auto
       with \<open>card {0..m-1} = m\<close> have equal_card: "card (g ` {0..m-1}) = card {0..m-1}" by auto
       have "finite (g ` {0..m-1})" using image_size by auto
       with equal_card image_subset have "g ` {0..m-1} = {0..m-1}"
         by (metis card_image card_subset_eq finite_atLeastAtMost_int image_int_atLeastAtMost inj_on_of_nat of_nat_0)
       hence "i \<in> {0..m-1} \<Longrightarrow> \<exists> j \<in> {0..m-1}. i = g j" for i by auto
       hence "i \<in> {0..m-1} \<Longrightarrow> \<exists> j \<in> {0..m-1}. i = (f j) mod m" for i
-        using \<open>g \<equiv> \<lambda>i. f i mod int m\<close> by auto  
+        using \<open>g \<equiv> \<lambda>i. f i mod int m\<close> by auto
       hence surj: "i \<in> {0..m-1} \<Longrightarrow> \<exists> j \<in> {0..m-1}. [i = f j] (mod m)" for i
         by (metis mod_mod_trivial unique_euclidean_semiring_class.cong_def)
       have "S mod m \<ge> 0" using m_pos by simp
       moreover have "S mod m \<le> m-1"
         using m_pos by (simp add: of_nat_diff)
       ultimately have "S mod m \<in> {0..m-1}" by auto
       with surj m_pos have "\<exists> j \<in> {0..m-1}. [S mod m = f j] (mod m)"
         by (metis atLeastAtMost_iff less_eq_nat.simps(1) nonneg_int_cases of_nat_less_iff verit_comp_simplify(3))
       thus ?thesis using cong_mod_right cong_sym by blast
     qed
     have thm_odd_n: ?thesis if "odd N"
     proof -
       have "\<exists> b::int. [N = b] (mod m) \<and> odd b \<and> b \<in> I"
       proof -
         from complete_cong_class have "\<exists> i. i \<in> {0..m-1} \<and> [f i = N] (mod m)" by blast
         then obtain c::nat where c_def: "c \<in> {0..m-1} \<and> [f c = N] (mod m)" by auto
         define b::int where "b = f c"
         have "[N = b] (mod m)" using b_def c_def by (metis cong_sym)
         moreover have "odd b"
         proof
           assume "even b"
           have "\<exists>k::int. N = b + k*m" using \<open>[N = b] (mod m)\<close>
           by (metis cong_iff_lin cong_sym_eq mult.commute)
           then obtain k::int where k_def: "N = b + k*m" by auto
           have "even (k*m)" using even_m by auto
           hence "even N" using k_def \<open>even b\<close> by presburger
           thus False using \<open>odd N\<close> by blast
-        qed      
+        qed
         moreover have "b \<in> I" using b_def f_def c_def by auto
         ultimately show ?thesis by auto
       qed
       then obtain b::int where b_def: "[N = b] (mod m) \<and> odd b \<and> b \<in> I" by auto
       have "m^3 \<ge> m" using m_pos by (auto simp add: power3_eq_cube)
       hence "N \<ge> 28*m" using assms(1,2) by linarith
       hence "N \<ge> 2*m" by simp
       have "m^3 \<ge> 3*3*(3::nat)" using assms(1)
         by (metis power3_eq_cube power_mono zero_le_numeral)
       hence "N \<ge> 28*3*3*(3::nat)" using assms(2) by auto
       hence "N \<ge> 9" by simp
       hence "\<exists>k1 k2 k3 k4. N = polygonal_number m k1 + polygonal_number m k2 + polygonal_number m k3 + polygonal_number m k4"
         using sum_of_four_polygonal_numbers assms(1) b_def I_def \<open>N \<ge> 2 * m\<close> \<open>N \<ge> 9\<close> by blast
       then obtain k1 k2 k3 k4 where "N = polygonal_number m k1 + polygonal_number m k2 + polygonal_number m k3 + polygonal_number m k4" by blast
-      moreover have "polygonal_number m 0 = 0" using Polygonal_Number_Theorem_Gauss.polygonal_number_def by auto  
+      moreover have "polygonal_number m 0 = 0" using Polygonal_Number_Theorem_Gauss.polygonal_number_def by auto
       ultimately have "N = polygonal_number m k1 + polygonal_number m k2 + polygonal_number m k3 + polygonal_number m k4 + polygonal_number m 0" by linarith
       thus ?thesis by blast
     qed
     have thm_even_n: ?thesis if "even N"
     proof -
       have "\<exists> b::int. [N-1 = b] (mod m) \<and> odd b \<and> b \<in> I"
       proof -
-        from complete_cong_class have "\<exists> i. i \<in> {0..m-1} \<and> [f i = N-1] (mod m)" by blast 
+        from complete_cong_class have "\<exists> i. i \<in> {0..m-1} \<and> [f i = N-1] (mod m)" by blast
         then obtain c::nat where c_def: "c \<in> {0..m-1} \<and> [f c = N-1] (mod m)" by auto
         define b::int where "b = f c"
         have "[N-1 = b] (mod m)" using b_def c_def by (metis cong_sym)
         moreover have "odd b"
         proof
           assume "even b"
           have "\<exists>k::int. N-1 = b + k*m" using \<open>[N-1 = b] (mod m)\<close>
           by (metis (full_types) cong_iff_lin cong_sym_eq mult.commute)
           then obtain k::int where k_def: "N-1 = b + k*m" by auto
           have "even (k*m)" using even_m by auto
           hence "even (N-1)" using k_def \<open>even b\<close> by presburger
           hence "odd N"
             by (metis Groups.mult_ac(2) \<open>2 * m \<le> N\<close> add_eq_self_zero add_leD1 assms(1) dvd_diffD1 le_trans mult_2_right nat_1_add_1 nat_dvd_1_iff_1 rel_simps(25) zero_neq_numeral)
           thus False using \<open>even N\<close> by blast
         qed
         moreover have "b \<in> I" using b_def f_def c_def by auto
         ultimately show ?thesis by auto
       qed
       then obtain b::int where b_def: "[N-1 = b] (mod m) \<and> odd b \<and> b \<in> I" by auto
       from b_def have "b \<in> I" by auto
       define a::int where a_def: "a = 2*(N-1-b) div m + b"
       have "m dvd (N-1-b)" using b_def
         by (smt (verit, ccfv_threshold) cong_iff_dvd_diff zdvd_zdiffD)
       hence "even (2*(N-1-b) div m)"
         by (metis div_mult_swap dvd_triv_left)
-      hence "odd a" using a_def b_def by auto 
+      hence "odd a" using a_def b_def by auto
       from assms(1) have "m^3 \<ge> m"
         by (simp add: power3_eq_cube)
       hence "N \<ge> 2 * m" using assms(1,2) by simp
       from assms(1) have m_pos: "m > 0" by auto
       have "N-1 \<ge> b"
       proof -
         from assms(1) have "m \<ge> 1" by auto
         hence "1/m \<le> 1" using m_pos by auto
         moreover have "N > 0" using \<open>N \<ge> 2 * m\<close> m_pos by auto
         ultimately have "N/m \<le> N"
           using divide_less_eq_1 less_eq_real_def by fastforce
         hence "sqrt(8*N/m - 8) \<le> sqrt(8*(N-1))" by auto
         from assms(1) have "m^3 \<ge> 3*3*(3::real)"
           by (metis numeral_le_real_of_nat_iff numeral_times_numeral power3_eq_cube power_mono zero_le_numeral)
         hence "N \<ge> 28*3*3*(3::real)" using assms(2) by linarith
         hence "N-6 \<ge> 6" by simp
-        hence "N-6 \<ge> 0" by simp  
+        hence "N-6 \<ge> 0" by simp
         with \<open>N-6 \<ge> 6\<close> have "(N-6)^2 \<ge> 6^2"
           using power2_nat_le_eq_le by blast
         hence "(N-6)^2 \<ge> 24" by simp
         hence "(N-2)^2 \<ge> 8*(N-1)" by (simp add: power2_eq_square algebra_simps)
         hence "(N-2) \<ge> sqrt (8*(N-1))" using \<open>N > 0\<close>
           by (metis of_nat_0_le_iff of_nat_mono of_nat_power real_sqrt_le_mono real_sqrt_pow2 real_sqrt_power)
         hence "N - (2::real) - sqrt(8*N/m - 8) \<ge> 0"
           using \<open>sqrt (real (8 * N) / real m - 8) \<le> sqrt (real (8 * (N - 1)))\<close> \<open>N-6 \<ge> 6\<close> by linarith
         hence expr_pos: "N - 1 - (2/3::real) - sqrt(8*N/m - 8) \<ge> 0" by auto
         have "b \<le> 2/3 + sqrt(8*N/m - 8)" using \<open>b \<in> I\<close> I_def by auto
         hence "N - 1 - b \<ge> N - 1 - (2/3 + sqrt(8*N/m-8))" by auto
         hence "N - 1 - b \<ge> 0"
           using expr_pos of_int_0_le_iff by auto
         thus ?thesis by auto
       qed
       from \<open>N \<ge> 2 * m\<close> m_pos have "6*N/m - 3 \<ge> 0" by (simp add: mult_imp_le_div_pos)
       hence "1/2 + sqrt (6*N/m - 3) > 0"
-        by (smt (verit, del_insts) divide_le_0_1_iff real_sqrt_ge_zero) 
+        by (smt (verit, del_insts) divide_le_0_1_iff real_sqrt_ge_zero)
       with \<open>b \<in> I\<close> b_def I_def have "b \<ge> 1" by auto
       hence b_pos: "b \<ge> 0" by auto
       from \<open>b \<in> I\<close> have b_in_I: "(1/2::real) + sqrt (6* real N / real m - 3) \<le> b \<and> b \<le> (2/3::real) + sqrt (8 * real N/real m - 8)" unfolding I_def by auto
       from b_pos \<open>N-1 \<ge> b\<close> a_def have a_pos: "a \<ge> 0"
         by (smt (verit) m_pos of_nat_0_less_iff pos_imp_zdiv_neg_iff)
       hence "a \<ge> 1"
         by (smt (verit) \<open>odd a\<close> dvd_0_right)
       have "a - b = 2*(N-1-b) div m" using a_def by auto
       from \<open>int m dvd (N - 1 - b)\<close> have "m dvd 2*(N-1-b)" by fastforce
       have "a = 2*(N-1-b)/m + b" using a_def m_pos
         using \<open>int m dvd 2 * (N - 1 - b)\<close> by fastforce
-      hence "a = 2*(N-1)/m - 2*b/m + b" 
+      hence "a = 2*(N-1)/m - 2*b/m + b"
         by (simp add: assms diff_divide_distrib of_nat_diff)
       hence "(2::real)*(N-1)/m = a + 2*b/m - b" by auto
       hence "(2::real)*(N-1) = (a + 2*b/m - b)*m"
         using m_pos by (simp add: divide_eq_eq)
       hence "(2::real)*(N-1) = m*(a-b) + 2*b"
         using \<open>int m dvd 2 * (N - 1 - b)\<close> a_def by auto
       hence "N-1 = m*(a-b)/2 + b" by auto
       hence "N = m*(a-b)/2 + b + 1"
         using \<open>2 * m \<le> N\<close> assms(1) by linarith
       hence N_expr: "N = real m * (of_int a - of_int b) / 2 + of_int b + 1" by auto
       have "even (a-b)" using \<open>odd a\<close> b_def by auto
       hence "2 dvd m*(a-b)" by auto
       hence N_expr2: "N = m*(a-b) div 2 + b + 1" using \<open>N = m*(a-b)/2 + b + 1\<close> by linarith
       define Nr where "Nr = real_of_nat N"
       define mr where "mr = real m"
       define ar where "ar = real_of_int a"
       define br where "br = real_of_int b"
       from assms(1) have "mr \<ge> 3" using mr_def by auto
       moreover have "Nr \<ge> 2*mr" using Nr_def mr_def \<open>N \<ge> 2 * m\<close> by auto
       moreover have "br \<ge> 0" using br_def b_pos by auto
       moreover have "mr > 0" using mr_def m_pos by auto
       moreover have "ar \<ge> 0" using ar_def \<open>a \<ge> 0\<close> by auto
       moreover have "Nr = mr*(ar-br)/2 + br + 1" using Nr_def mr_def ar_def br_def N_expr by auto
       moreover have "1/2 + sqrt (6*Nr/mr-3) \<le> br \<and> br \<le> 2/3 + sqrt (8*Nr/mr-8)" using Nr_def mr_def br_def b_in_I by auto
       ultimately have "br^2 < 4*ar \<and> 3*ar < br^2+2*br+4" using Cauchy_lemma
         by auto
-      hence real_ineq:"(real_of_int b)^2 < 4*(real_of_int a) \<and> 3*(real_of_int a) < (real_of_int b)^2 + 2*(real_of_int b) + 4" 
+      hence real_ineq:"(real_of_int b)^2 < 4*(real_of_int a) \<and> 3*(real_of_int a) < (real_of_int b)^2 + 2*(real_of_int b) + 4"
         using br_def ar_def by auto
       hence int_ineq1: "b^2<4*a" using of_int_less_iff by fastforce
       from real_ineq have int_ineq2: "3*a < b^2+2*b+4" using of_int_less_iff by fastforce
-    
+
       define an:: nat where "an = nat a"
       from a_pos have "an = a" unfolding an_def by auto
       define bn:: nat where "bn = nat b"
       from b_pos have "bn = b" unfolding bn_def by auto
       have "an \<ge> 1" using \<open>int an = a\<close> \<open>a \<ge> 1\<close> by auto
       moreover have "bn \<ge> 1" using \<open>int bn = b\<close> \<open>b \<ge> 1\<close> by auto
       moreover have "odd an" using \<open>odd a\<close> \<open>int an = a\<close> by auto
       moreover have "odd bn" using b_def \<open>int bn = b\<close> by auto
       moreover have "bn ^ 2 < 4 * an" using int_ineq1 \<open>int an = a\<close> \<open>int bn = b\<close>
         using of_nat_less_iff by fastforce
       moreover have "3 * an < bn ^ 2 + 2 * bn + 4" using int_ineq2 \<open>int an = a\<close> \<open>int bn = b\<close>
         using of_nat_less_iff by fastforce
       ultimately have "\<exists>s t u v :: int. s \<ge> 0 \<and> t \<ge> 0 \<and> u \<ge> 0 \<and> v \<ge> 0 \<and> an = s^2 + t^2 + u^2 + v^2 \<and>
     bn = s+t+u+v" using four_nonneg_int_sum by auto
       hence "\<exists>s t u v :: int. s \<ge> 0 \<and> t \<ge> 0 \<and> u \<ge> 0 \<and> v \<ge> 0 \<and> a = s^2 + t^2 + u^2 + v^2 \<and>
     b = s+t+u+v" using \<open>int an = a\<close> \<open>int bn = b\<close> by auto
       then obtain s t u v :: int where stuv: "s \<ge> 0 \<and> t \<ge> 0 \<and> u \<ge> 0 \<and> v \<ge> 0 \<and> a = s^2 + t^2 + u^2 + v^2 \<and>
     b = s+t+u+v" by auto
       hence "N = (m*(s^2+t^2+u^2+v^2-s-t-u-v) div 2) + s+t+u+v + 1" using N_expr2 by (smt (verit, ccfv_threshold))
       hence "N = (m*(s^2-s+t^2-t+u^2-u+v^2-v) div 2) + s+t+u+v + 1" by (smt (verit, ccfv_SIG))
       hence "N = (m * (s * (s-1) + t * (t-1) + u * (u-1) + v * (v-1)) div 2) +s+t+u+v + 1" by (simp add: power2_eq_square algebra_simps)
       hence previous_step: "N = (m * s * (s-1) + m * t * (t-1) + m * u * (u-1) + m * v * (v-1)) div 2 + s+t+u+v + 1" by (simp add: algebra_simps)
       moreover have "2 dvd m * s * (s-1)" by simp
       moreover have "2 dvd m * t * (t-1)" by simp
       moreover have "2 dvd m * u * (u-1)" by simp
       moreover have "2 dvd m * v * (v-1)" by simp
       ultimately have "N = m * s * (s-1) div 2 + m * t * (t-1) div 2 + m * u * (u-1) div 2 + m * v *(v-1) div 2 + s+t+u+v + 1" by fastforce
       hence N_expr3: "N = m * s * (s-1) div 2 + s + m * t * (t-1) div 2 + t + m * u * (u-1) div 2 + u + m * v * (v-1) div 2 + v + 1" by auto
       define sn::nat where "sn = nat s"
       define tn::nat where "tn = nat t"
       define un::nat where "un = nat u"
       define vn::nat where "vn = nat v"
       have "sn = s" using stuv sn_def by auto
       hence "m * sn * (sn-1) = m * s * (s-1)" by fastforce
       hence "m * sn * (sn-1) div 2 = m * s * (s-1) div 2" by linarith
       have "tn = t" using stuv tn_def by auto
       hence "m * tn * (tn-1) = m * t * (t-1)" by fastforce
       hence "m * tn * (tn-1) div 2 = m * t * (t-1) div 2" by linarith
       have "un = u" using stuv un_def by auto
       hence "m * un * (un-1) = m * u * (u-1)" by fastforce
       hence "m * un * (un-1) div 2 = m * u * (u-1) div 2" by linarith
       have "vn = v" using stuv vn_def by auto
       hence "m * vn * (vn-1) = m * v * (v-1)" by fastforce
       hence "m * vn * (vn-1) div 2 = m * v * (v-1) div 2" by linarith
       have "N = m * sn * (sn-1) div 2 + sn + m * tn * (tn-1) div 2 + tn + m * un * (un-1) div 2 + un + m * vn * (vn-1) div 2 + vn + 1"
         using N_expr3 \<open>sn = s\<close> \<open>tn = t\<close> \<open>un = u\<close> \<open>vn = v\<close> \<open>m * sn * (sn-1) div 2 = m * s * (s-1) div 2\<close> \<open>m * tn * (tn-1) div 2 = m * t * (t-1) div 2\<close> \<open>m * un * (un-1) div 2 = m * u * (u-1) div 2\<close> \<open>m * vn * (vn-1) div 2 = m * v * (v-1) div 2\<close> by linarith
       hence "N = polygonal_number m sn + polygonal_number m tn + polygonal_number m un + polygonal_number m vn + 1"
         using Polygonal_Number_Theorem_Gauss.polygonal_number_def by presburger
       also have "polygonal_number m 1 = 1" using Polygonal_Number_Theorem_Gauss.polygonal_number_def by auto
       ultimately have "N = polygonal_number m sn + polygonal_number m tn + polygonal_number m un + polygonal_number m vn + polygonal_number m 1" by auto
       thus ?thesis by blast
     qed
     show ?thesis using thm_odd_n thm_even_n by blast
   qed
 qed
 end
\ No newline at end of file
diff --git a/thys/Polygonal_Number_Theorem/ROOT b/thys/Polygonal_Number_Theorem/ROOT
--- a/thys/Polygonal_Number_Theorem/ROOT
+++ b/thys/Polygonal_Number_Theorem/ROOT
@@ -1,17 +1,14 @@
 chapter AFP
 
-session "Polygonal_Number_Theorem" (AFP) = "HOL-Analysis" +
+session "Polygonal_Number_Theorem" (AFP) = "Three_Squares" +
   options [timeout = 600]
 
-  sessions
-    "Three_Squares"
-
   theories
     "Polygonal_Number_Theorem_Lemmas"
     "Polygonal_Number_Theorem_Gauss"
     "Polygonal_Number_Theorem_Cauchy"
     "Polygonal_Number_Theorem_Legendre"
-    
+
   document_files
     "root.tex"
     "root.bib"
\ No newline at end of file
diff --git a/thys/Quantales_Converse/Modal_Quantale.thy b/thys/Quantales_Converse/Modal_Quantale.thy
--- a/thys/Quantales_Converse/Modal_Quantale.thy
+++ b/thys/Quantales_Converse/Modal_Quantale.thy
@@ -1,329 +1,329 @@
-(* 
+(*
 Title: Modal quantales
 Author: Georg Struth
 Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
 *)
 
 section \<open>Modal quantales\<close>
 
 theory Modal_Quantale
   imports Quantales.Quantale_Star Modal_Kleene_Algebra_Var KAD.Modal_Kleene_Algebra
 
 begin
 
 subsection \<open>Simplified modal semirings and Kleene algebras\<close>
 
-text \<open>The previous formalisation of modal Kleene algebra in the AFP adds two compatibility axioms between domain and codomain 
-when combining an antidomain semiring with an antirange semiring. But these are unnecessary. They are derivable from the other 
+text \<open>The previous formalisation of modal Kleene algebra in the AFP adds two compatibility axioms between domain and codomain
+when combining an antidomain semiring with an antirange semiring. But these are unnecessary. They are derivable from the other
 axioms. Thus I provide a simpler axiomatisation that should eventually replace the one in the AFP.\<close>
 
 class modal_semiring_simp = antidomain_semiring + antirange_semiring
 
 lemma (in modal_semiring_simp) dr_compat [simp]: "d (r x) = r x"
 proof-
   have a: "ar x \<cdot> d (r x) = 0"
     using local.ads_d_def local.ars_r_def local.dpdz.dom_weakly_local by auto
   have "r x \<cdot> d (r x) \<cdot> ar x \<le> r x \<cdot> ar x"
     by (simp add: local.a_subid_aux2 local.ads_d_def local.mult_isor)
   hence b: "r x \<cdot> d (r x) \<cdot> ar x = 0"
     by (simp add: local.ardual.am2 local.ars_r_def local.join.bot_unique)
   have "d (r x) = (ar x + r x) \<cdot> d (r x)"
     using local.add_comm local.ardual.ans3 local.ars_r_def local.mult_1_left by presburger
   also have "\<dots> = ar x \<cdot> d (r x) + r x \<cdot> d (r x)"
     by simp
   also have "\<dots> = r x \<cdot> d (r x)"
     by (simp add: a)
   also have "\<dots> = r x \<cdot> d (r x) \<cdot> (ar x + r x)"
     using local.add_comm local.ardual.ans3 local.ars_r_def by auto
   also have "\<dots> = r x \<cdot> d (r x) \<cdot> ar x + r x \<cdot> d (r x) \<cdot> r x"
     by simp
   also have "\<dots> = r x \<cdot> d (r x) \<cdot> r x"
     using b by auto
   also have "\<dots> = r x"
     by (metis local.ads_d_def local.am3 local.ardual.a_mult_idem local.ars_r_def local.ds.ddual.mult_assoc)
   finally show ?thesis
     by simp
 qed
 
 lemma (in modal_semiring_simp) rd_compat [simp]: "r (d x) = d x"
   by (smt (verit) local.a_mult_idem local.ads_d_def local.am2 local.ardual.dpdz.dom_weakly_local local.ars_r_def local.dr_compat local.kat_3_equiv')
 
 subclass (in modal_semiring_simp) modal_semiring
   apply unfold_locales by simp_all
 
 class modal_kleene_algebra_simp = modal_semiring_simp + kleene_algebra
 
 subclass (in modal_kleene_algebra_simp) modal_kleene_algebra..
 
 
 subsection \<open>Domain quantales\<close>
 
 class domain_quantale = unital_quantale + domain_op +
   assumes dom_absorb: "x \<le> dom x \<cdot> x"
   and dom_local: "dom (x \<cdot> dom y) = dom (x \<cdot> y)"
   and dom_add: "dom (x \<squnion> y) = dom x \<squnion> dom y"
   and dom_subid: "dom x \<le> 1"
   and dom_zero [simp]: "dom \<bottom> = \<bottom>"
 
-text \<open>The definition is that of a domain semiring. I cannot extend the quantale class with respect to domain semirings 
+text \<open>The definition is that of a domain semiring. I cannot extend the quantale class with respect to domain semirings
 because of different operations are used for addition/sup. The following sublocale statement brings all those properties into scope.\<close>
 
 sublocale domain_quantale \<subseteq> dqmsr: domain_semiring "(\<squnion>)" "(\<cdot>)" 1 \<bottom> dom "(\<le>)" "(<)"
   by unfold_locales (simp_all add: dom_add dom_local dom_absorb sup.absorb2 dom_subid)
 
 sublocale domain_quantale \<subseteq> dqmka: domain_kleene_algebra "(\<squnion>)" "(\<cdot>)" 1 \<bottom>  dom "(\<le>)" "(<)" qstar..
 
 typedef (overloaded)  'a d_element = "{x :: 'a :: domain_quantale. dom x = x}"
   using dqmsr.dom_one by blast
 
 setup_lifting type_definition_d_element
 
 instantiation d_element :: (domain_quantale) bounded_lattice
 
 begin
 
 lift_definition less_eq_d_element :: "'a d_element \<Rightarrow> 'a d_element \<Rightarrow> bool" is "(\<le>)" .
 
 lift_definition less_d_element :: "'a d_element \<Rightarrow> 'a d_element \<Rightarrow> bool" is "(<)" .
 
 lift_definition bot_d_element :: "'a d_element" is \<bottom>
   by simp
 
 lift_definition top_d_element :: "'a d_element" is 1
   by simp
 
 lift_definition inf_d_element :: "'a d_element \<Rightarrow> 'a d_element \<Rightarrow> 'a d_element" is "(\<cdot>)"
   by (metis dqmsr.dom_mult_closed)
 
 lift_definition sup_d_element :: "'a d_element \<Rightarrow> 'a d_element \<Rightarrow> 'a d_element" is "(\<squnion>)"
   by simp
 
 instance
   apply (standard; transfer)
              apply (simp_all add: less_le_not_le)
      apply (metis dqmsr.dom_subid_aux2'')
     apply (metis dqmsr.dom_subid_aux1'')
    apply (metis dqmsr.dom_glb_eq)
   by (metis dqmsr.dom_subid)
 
 end
 
 instance d_element :: (domain_quantale) distrib_lattice
   by (standard, transfer, metis dqmsr.dom_distrib)
 
 context domain_quantale
 begin
 
 lemma dom_top [simp]: "dom \<top> = 1"
 proof-
   have "1 \<le> \<top>"
     by simp
   hence "dom 1 \<le> dom \<top>"
     using local.dqmsr.d_iso by blast
   thus ?thesis
     by (simp add: local.dual_order.antisym)
 qed
 
 lemma dom_top2: "x \<cdot> \<top> \<le> dom x \<cdot> \<top>"
 proof-
   have "x \<cdot> \<top> = dom x \<cdot> x \<cdot> \<top>"
     by simp
   also have "\<dots> \<le> dom x \<cdot> \<top> \<cdot> \<top>"
     using local.dqmsr.d_restrict_iff_1 local.top_greatest local.top_times_top mult_assoc by presburger
   finally show ?thesis
     by (simp add: local.mult.semigroup_axioms semigroup.assoc)
 qed
 
 lemma weak_twisted: "x \<cdot> dom y \<le> dom (x \<cdot> y) \<cdot> x"
   using local.dqmsr.fd_def local.dqmsr.fdemodalisation2 local.eq_refl by blast
 
 lemma dom_meet: "dom x \<cdot> dom y = dom x \<sqinter> dom y"
   apply (rule order.antisym)
    apply (simp add: local.dqmsr.dom_subid_aux2 local.dqmsr.dom_subid_aux2'')
   by (smt (z3) local.dom_absorb local.dqmsr.dom_iso local.dqmsr.dom_subid_aux2 local.dqmsr.dsg3 local.dqmsr.dsg4 local.dual_order.antisym local.inf.cobounded1 local.inf.cobounded2 local.psrpq.mult_isol_var)
 
 lemma dom_meet_pres: "dom (dom x \<sqinter> dom y) = dom x \<sqinter> dom y"
   using dom_meet local.dqmsr.dom_mult_closed by presburger
 
 lemma dom_meet_distl: "dom x \<cdot> (y \<sqinter> z) = (dom x \<cdot> y) \<sqinter> (dom x \<cdot> z)"
 proof-
   have a: "dom x \<cdot> (y \<sqinter> z) \<le> (dom x \<cdot> y) \<sqinter> (dom x \<cdot> z)"
     using local.mult_isol by force
   have "(dom x \<cdot> y) \<sqinter> (dom x \<cdot> z) = dom ((dom x \<cdot> y) \<sqinter> (dom x \<cdot> z)) \<cdot> ((dom x \<cdot> y) \<sqinter> (dom x \<cdot> z))"
     by simp
   also have "\<dots> \<le> dom ((dom x \<cdot> y)) \<cdot> ((dom x \<cdot> y) \<sqinter> (dom x \<cdot> z))"
     using calculation local.dqmsr.dom_iso local.dqmsr.dom_llp2 local.inf.cobounded1 by presburger
   also have "\<dots> \<le> dom x \<cdot> ((dom x \<cdot> y) \<sqinter> (dom x \<cdot> z))"
     by (metis local.dqmsr.domain_1'' local.dqmsr.domain_invol local.mult_isor)
   also have "\<dots> \<le> dom x \<cdot> (y \<sqinter> z)"
     by (meson local.dqmsr.dom_subid_aux2 local.inf_mono local.order_refl local.psrpq.mult_isol_var)
   finally show ?thesis
     using a local.dual_order.antisym by blast
 qed
 
 lemma dom_meet_approx: "dom ((dom x \<cdot> y) \<sqinter> (dom x \<cdot> z)) \<le> dom x"
   by (metis dom_meet_distl local.dqmsr.domain_1'' local.dqmsr.domain_invol)
 
 lemma dom_inf_pres_aux: "Y \<noteq> {} \<Longrightarrow> dom (\<Sqinter>y \<in> Y. dom x \<cdot> y) \<le> dom x"
 proof-
   assume "Y \<noteq> {}"
   have "\<forall>z\<in>Y. dom (\<Sqinter>y \<in> Y. dom x \<cdot> y) \<le> dom (dom x \<cdot> z)"
     by (meson local.INF_lower local.dqmsr.dom_iso)
   hence "\<forall>z\<in>Y. dom (\<Sqinter>y \<in> Y. dom x \<cdot> y) \<le> dom x \<cdot> dom z"
     by fastforce
   hence "\<forall>z\<in>Y. dom (\<Sqinter>y \<in> Y. dom x \<cdot> y) \<le> dom x"
     using dom_meet by fastforce
   thus "dom (\<Sqinter>y \<in> Y. dom x \<cdot> y) \<le> dom x"
     using \<open>Y \<noteq> {}\<close> by blast
 qed
 
 lemma dom_inf_pres_aux2: "(\<Sqinter>y \<in> Y. dom x \<cdot> y) \<le> \<Sqinter>Y"
   by (simp add: local.INF_lower2 local.dqmsr.dom_subid_aux2 local.le_Inf_iff)
 
 lemma dom_inf_pres: "Y \<noteq> {} \<Longrightarrow> dom x \<cdot> (\<Sqinter>Y) = (\<Sqinter>y \<in> Y. dom x \<cdot> y)"
 proof-
   assume hyp: "Y \<noteq> {}"
   have a: "dom x \<cdot> (\<Sqinter>Y) \<le> (\<Sqinter>y \<in> Y. dom x \<cdot> y)"
     by (simp add: Setcompr_eq_image local.Inf_subdistl)
   have "(\<Sqinter>y \<in> Y. dom x \<cdot> y) = dom (\<Sqinter>y \<in> Y. dom x \<cdot> y) \<cdot> (\<Sqinter>y \<in> Y. dom x \<cdot> y)"
     by simp
   also have "\<dots> \<le> dom x \<cdot> (\<Sqinter>y \<in> Y. dom x \<cdot> y)"
     using dom_inf_pres_aux hyp local.mult_isor by blast
   also have "\<dots> \<le> dom x \<cdot> \<Sqinter>Y"
     by (simp add: dom_inf_pres_aux2 local.psrpq.mult_isol_var)
   finally show ?thesis
     using a order.antisym by blast
 qed
 
 lemma "dom (\<Sqinter>X) \<le> \<Sqinter> (dom ` X)"
   by (simp add: local.INF_greatest local.Inf_lower local.dqmsr.dom_iso)
 
 text \<open>The domain operation need not preserve arbitrary sups, though this property holds, for instance,
 in quantales of binary relations. I do not aim at a stronger axiomatisation in this theory.\<close>
 
 lemma dom_top_pres: "(x \<le> dom y \<cdot> x) = (x \<le> dom y \<cdot> \<top>)"
   apply standard
    apply (meson local.dqmsr.ddual.mult_isol_var local.dual_order.eq_iff local.dual_order.trans local.top_greatest)
   using local.dqmsr.dom_iso local.dqmsr.dom_llp by fastforce
 
 lemma dom_lla_var: "(dom x \<le> dom y) = (x \<le> dom y \<cdot> \<top>)"
   using dom_top_pres local.dqmsr.dom_llp by force
 
 lemma "dom (1 \<sqinter> x) = 1 \<sqinter> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> dom x = x"
   using local.inf_absorb2 by force
 
 lemma dom_meet_sub: "dom (x \<sqinter> y) \<le> dom x \<sqinter> dom y"
   by (simp add: local.dqmsr.d_iso)
 
 lemma dom_dist1: "dom x \<squnion> (dom y \<sqinter> dom z) = (dom x \<squnion> dom y) \<sqinter> (dom x \<squnion> dom z)"
   by (metis dom_meet local.dom_add local.dqmsr.dom_distrib)
 
 lemma dom_dist2: "dom x \<sqinter> (dom y \<squnion> dom z) = (dom x \<sqinter> dom y) \<squnion> (dom x \<sqinter> dom z)"
   by (metis dom_meet local.dom_add local.sup_distl)
 
 abbreviation "fd' \<equiv> dqmsr.fd"
 
 definition "bb x y = \<Squnion>{dom z |z. fd' x z \<le> dom y}"
 
 lemma fd'_bb_galois_aux: "fd' x (dom p) \<le> dom q \<Longrightarrow> dom p \<le> bb x (dom q)"
   by (simp add: bb_def local.SUP_upper setcompr_eq_image)
 
 lemma dom_iso_var: "(\<Squnion>x \<in> X. dom x) \<le> dom (\<Squnion>x \<in> X. dom x)"
   by (meson local.SUP_le_iff local.dom_subid local.dqmsr.domain_subid)
 
 lemma dom_iso_var2: "(\<Squnion>x \<in> X. dom x) \<le> dom (\<Squnion>x \<in> X. x)"
   by (simp add: local.SUP_le_iff local.Sup_upper local.dqmsr.dom_iso)
 
 end
 
 
 subsection \<open>Codomain quantales\<close>
 
 class codomain_quantale = unital_quantale + range_op +
-  assumes cod_absorb: "x \<le> x \<cdot> cod x" 
+  assumes cod_absorb: "x \<le> x \<cdot> cod x"
   and cod_local: "cod (cod x \<cdot> y) = cod (x \<cdot> y)"
   and cod_add: "cod (x \<squnion> y) = cod x \<squnion> cod y"
   and cod_subid: "cod x \<le> 1"
   and cod_zero: "cod \<bottom> = \<bottom>"
 
 sublocale codomain_quantale \<subseteq> coddual: domain_quantale range_op _ "\<lambda>x y. y \<cdot> x" _ _ _ _ _ _ _ _
   by unfold_locales (auto simp: mult_assoc cod_subid cod_zero cod_add cod_local cod_absorb Sup_distr Sup_distl)
 
 abbreviation (in codomain_quantale) "bd' \<equiv> coddual.fd'"
 
 definition (in codomain_quantale) "fb x y = \<Squnion>{cod z |z. bd' x z \<le> cod y}"
 
 lemma (in codomain_quantale) bd'_fb_galois_aux: "bd' x (cod p) \<le> cod q \<Longrightarrow> cod p \<le> fb x (cod q)"
   using local.coddual.bb_def local.coddual.fd'_bb_galois_aux local.fb_def by auto
 
 
 subsection \<open>Modal quantales\<close>
 
 class dc_modal_quantale = domain_quantale + codomain_quantale +
-  assumes dc_compat [simp]: "dom (cod x) = cod x" 
-  and cd_compat [simp]: "cod (dom x) = dom x" 
+  assumes dc_compat [simp]: "dom (cod x) = cod x"
+  and cd_compat [simp]: "cod (dom x) = dom x"
 
 sublocale dc_modal_quantale \<subseteq> mqs: dr_modal_kleene_algebra "(\<squnion>)" "(\<cdot>)" 1 \<bottom> "(\<le>)" "(<)" qstar dom cod
   by unfold_locales simp_all
 
 sublocale dc_modal_quantale \<subseteq> mqdual: dc_modal_quantale _ "\<lambda>x y. y \<cdot> x" _ _ _ _ _ _ _ _  dom cod
   by unfold_locales simp_all
 
 lemma (in dc_modal_quantale) "x \<cdot> \<top> = dom x \<cdot> \<top>"
 (*  nitpick[expect=genuine] *)
-  oops 
+  oops
 
 lemma (in dc_modal_quantale) "\<top> \<cdot> x = \<top> \<cdot> cod x"
 (*  nitpick[expect=genuine] *)
-  oops 
+  oops
 
 
 subsection \<open>Antidomain and anticodomain quantales\<close>
 
-notation antidomain_op ("adom") 
+notation antidomain_op ("adom")
 
 class antidomain_quantale = unital_quantale + antidomain_op +
   assumes as1 [simp]: "adom x \<cdot> x = \<bottom>"
   and as2 [simp]: "adom (x \<cdot> y) \<le> adom (x \<cdot> adom (adom y))"
   and as3 [simp]: "adom (adom x) \<squnion> adom x = 1"
 
 definition (in antidomain_quantale) "ddom = adom \<circ> adom"
 
 sublocale antidomain_quantale \<subseteq> adqmsr: antidomain_semiring adom "(\<squnion>)" "(\<cdot>)" 1 \<bottom> "(\<le>)" "(<)"
   by unfold_locales (simp_all add: local.sup.absorb2)
 
 sublocale antidomain_quantale \<subseteq> adqmka: antidomain_kleene_algebra adom "(\<squnion>)" "(\<cdot>)" 1 \<bottom> "(\<le>)" "(<)" qstar..
 
 sublocale antidomain_quantale \<subseteq> addq: domain_quantale ddom
   by unfold_locales (simp_all add: ddom_def local.adqmsr.ans_d_def)
 
-notation antirange_op ("acod") 
+notation antirange_op ("acod")
 
 class anticodomain_quantale = unital_quantale + antirange_op +
   assumes ars1 [simp]: "x \<cdot> acod x = \<bottom>"
   and ars2 [simp]: "acod (x \<cdot> y) \<le> acod (acod (acod x) \<cdot> y)"
   and ars3 [simp]: "acod (acod x) \<squnion> acod x = 1"
 
 sublocale anticodomain_quantale \<subseteq> acoddual: antidomain_quantale acod _ "\<lambda>x y. y \<cdot> x" _ _ _ _ _ _ _ _
   by unfold_locales (auto simp: mult_assoc Sup_distl Sup_distr)
 
 definition (in anticodomain_quantale) "ccod = acod \<circ> acod"
 
 sublocale anticodomain_quantale \<subseteq> acdqmsr: antirange_semiring "(\<squnion>)" "(\<cdot>)" 1 \<bottom> acod "(\<le>)" "(<)"..
 
 sublocale anticodomain_quantale \<subseteq> acdqmka: antirange_kleene_algebra "(\<squnion>)" "(\<cdot>)" 1 \<bottom> "(\<le>)" "(<)" qstar acod..
 
 sublocale anticodomain_quantale \<subseteq> acddq: codomain_quantale _ _ _ _ _ _ _ _ _ _ "\<lambda> x. acod (acod x)"
   by unfold_locales (simp_all add: local.acoddual.adqmsr.ans_d_def)
 
 class modal_quantale = antidomain_quantale + anticodomain_quantale
 
 sublocale modal_quantale \<subseteq> mmqs: modal_kleene_algebra_simp "(\<squnion>)" "(\<cdot>)" 1 \<bottom> "(\<le>)" "(<)" qstar adom acod..
 
 sublocale modal_quantale \<subseteq> mmqdual: modal_quantale _ "\<lambda>x y. y \<cdot> x" _ _ _ _ _ _ _ _ adom acod
   by unfold_locales simp_all
 
 end
 
 
 
diff --git a/thys/Quantales_Converse/Quantale_Converse.thy b/thys/Quantales_Converse/Quantale_Converse.thy
--- a/thys/Quantales_Converse/Quantale_Converse.thy
+++ b/thys/Quantales_Converse/Quantale_Converse.thy
@@ -1,1583 +1,1583 @@
-(* 
+(*
 Title: Quantales with converse
 Author: Cameron Calk, Georg Struth
 Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
 *)
 
 section \<open>Quantales with converse\<close>
 
 theory Quantale_Converse
-  imports Modal_Quantale Modal_Kleene_Algebra_Converse 
+  imports Modal_Quantale Modal_Kleene_Algebra_Converse
 
 begin
 
 subsection \<open>Properties of unital quantales\<close>
 
 text \<open>These properties should eventually added to the quantales AFP entry.\<close>
 
 lemma (in quantale) bres_bot_top [simp]: "\<bottom> \<rightarrow> \<top> = \<top>"
   by (simp add: local.bres_galois_imp local.order.antisym)
 
 lemma (in quantale) fres_top_bot [simp]: "\<top> \<leftarrow> \<bottom> = \<top>"
   by (meson local.fres_galois local.order_antisym local.top_greatest)
 
 lemma (in unital_quantale) bres_top_top2 [simp]: "(x \<rightarrow> y \<cdot> \<top>) \<cdot> \<top> = x \<rightarrow> y \<cdot> \<top>"
 proof-
   have "(x \<rightarrow> y \<cdot> \<top>) \<cdot> \<top> \<le> x \<rightarrow> y \<cdot> \<top> \<cdot> \<top>"
     by (simp add: local.bres_interchange)
   hence "(x \<rightarrow> y \<cdot> \<top>) \<cdot> \<top> \<le> x \<rightarrow> y \<cdot> \<top>"
     by (simp add: mult_assoc)
   thus ?thesis
     by (metis local.mult_1_right local.order_eq_iff local.psrpq.subdistl local.sup_top_right)
 qed
 
 lemma (in unital_quantale) fres_top_top2 [simp]: "\<top> \<cdot> (\<top> \<cdot> y \<leftarrow> x) =  \<top> \<cdot> y \<leftarrow> x"
   by (metis local.dual_order.antisym local.fres_interchange local.le_top local.top_greatest mult_assoc)
 
 lemma (in unital_quantale) bres_top_bot [simp]: "\<top> \<rightarrow> \<bottom> = \<bottom>"
   by (metis local.bot_least local.bres_canc1 local.le_top local.order.antisym)
 
 lemma (in unital_quantale) fres_bot_top [simp]: "\<bottom> \<leftarrow> \<top> = \<bottom>"
   by (metis local.bot_unique local.fres_canc1 local.top_le local.uqka.independence2 local.uwqlka.star_ext)
 
 lemma (in unital_quantale) top_bot_iff: "(x \<cdot> \<top> = \<bottom>) = (x = \<bottom>)"
   by (metis local.fres_bot_top local.fres_canc2 local.le_bot local.mult_botl)
 
 
 subsection \<open>Involutive quantales\<close>
 
 text \<open>The following axioms for involutive quantales are standard.\<close>
 
 class involutive_quantale = unital_quantale + invol_op +
   assumes inv_invol [simp]: "(x\<^sup>\<circ>)\<^sup>\<circ> = x"
   and inv_contrav: "(x \<cdot> y)\<^sup>\<circ> = y\<^sup>\<circ> \<cdot> x\<^sup>\<circ>"
   and inv_sup [simp]: "(\<Squnion>X)\<^sup>\<circ> = (\<Squnion>x \<in> X. x\<^sup>\<circ>)"
 
 context involutive_quantale
 begin
 
 lemma inv_binsup [simp]: "(x \<squnion> y)\<^sup>\<circ> = x\<^sup>\<circ> \<squnion> y\<^sup>\<circ>"
 proof-
   have "(x \<squnion> y)\<^sup>\<circ> = (\<Squnion>z \<in> {x,y}. z\<^sup>\<circ>)"
     using local.inv_sup local.sup_Sup by presburger
   also have "\<dots> = (\<Squnion>z \<in> {x\<^sup>\<circ>,y\<^sup>\<circ>}. z)"
     by simp
   also have "\<dots> = x\<^sup>\<circ> \<squnion> y\<^sup>\<circ>"
     by fastforce
   finally show ?thesis.
 qed
 
 lemma inv_iso: "x \<le> y \<Longrightarrow> x\<^sup>\<circ> \<le> y\<^sup>\<circ>"
   by (metis inv_binsup local.sup.absorb_iff1)
 
 lemma inv_galois: "(x\<^sup>\<circ> \<le> y) = (x \<le> y\<^sup>\<circ>)"
   using local.inv_iso by fastforce
 
 lemma bres_fres_conv: "(y\<^sup>\<circ> \<leftarrow> x\<^sup>\<circ>)\<^sup>\<circ> = x \<rightarrow> y"
 proof-
   have "(y\<^sup>\<circ> \<leftarrow> x\<^sup>\<circ>)\<^sup>\<circ> = (\<Squnion>{z. z \<cdot> x\<^sup>\<circ> \<le> y\<^sup>\<circ>})\<^sup>\<circ>"
     by (simp add: local.fres_def)
   also have "\<dots> = \<Squnion>{z\<^sup>\<circ> |z. z \<cdot> x\<^sup>\<circ> \<le> y\<^sup>\<circ>}"
     by (simp add: image_Collect)
   also have "\<dots> = \<Squnion>{z. z\<^sup>\<circ> \<cdot> x\<^sup>\<circ> \<le> y\<^sup>\<circ>}"
     by (metis local.inv_invol)
   also have "\<dots> = \<Squnion>{z. (x \<cdot> z)\<^sup>\<circ> \<le> y\<^sup>\<circ>}"
     by (simp add: local.inv_contrav)
   also have "\<dots> = \<Squnion>{z. x \<cdot> z \<le> y}"
     by (metis local.inv_invol local.inv_iso)
   also have "\<dots> = x \<rightarrow> y"
     by (simp add: local.bres_def)
   finally show ?thesis.
 qed
 
 lemma fres_bres_conv: "(y\<^sup>\<circ> \<rightarrow> x\<^sup>\<circ>)\<^sup>\<circ> = x \<leftarrow> y"
   by (metis bres_fres_conv local.inv_invol)
 
 sublocale invqka: involutive_kleene_algebra "(\<squnion>)" "(\<cdot>)" 1 \<bottom> "(\<le>)" "(<)" qstar invol
   by unfold_locales (simp_all add: local.inv_contrav)
 
 lemma inv_binf [simp]: "(x \<sqinter> y)\<^sup>\<circ> = x\<^sup>\<circ> \<sqinter> y\<^sup>\<circ>"
 proof-
   {fix z
   have "(z \<le> (x \<sqinter> y)\<^sup>\<circ>) = (z\<^sup>\<circ> \<le> x \<sqinter> y)"
     using invqka.inv_adj by blast
   also have "\<dots> = (z\<^sup>\<circ> \<le> x \<and> z\<^sup>\<circ> \<le> y)"
     by simp
   also have "\<dots> = (z \<le> x\<^sup>\<circ> \<and> z \<le> y\<^sup>\<circ>)"
     by (simp add: invqka.inv_adj)
   also have "\<dots> = (z \<le> x\<^sup>\<circ> \<sqinter> y\<^sup>\<circ>)"
     by simp
   finally have "(z \<le> (x \<sqinter> y)\<^sup>\<circ>) = (z \<le> x\<^sup>\<circ> \<sqinter> y\<^sup>\<circ>)".}
   thus ?thesis
     using local.dual_order.antisym by blast
 qed
 
 lemma inv_inf [simp]: "(\<Sqinter>X)\<^sup>\<circ> = (\<Sqinter>x \<in> X. x\<^sup>\<circ>)"
   by (metis invqka.inv_adj local.INF_eqI local.Inf_greatest local.Inf_lower local.inv_invol)
 
 lemma inv_top [simp]: "\<top>\<^sup>\<circ> = \<top>"
 proof-
   have a: "\<top>\<^sup>\<circ> \<le> \<top>"
     by simp
   hence "(\<top>\<^sup>\<circ>)\<^sup>\<circ> \<le> \<top>\<^sup>\<circ>"
     using local.inv_iso by blast
   hence "\<top> \<le> \<top>\<^sup>\<circ>"
     by simp
   thus ?thesis
     by (simp add: local.top_le)
 qed
 
 lemma inv_qstar_aux [simp]: "(x ^ i)\<^sup>\<circ> = (x\<^sup>\<circ>) ^ i"
   by (induct i, simp_all add: local.power_commutes)
 
 lemma inv_conjugate: "(x\<^sup>\<circ> \<sqinter> y = \<bottom>) = (x \<sqinter> y\<^sup>\<circ> = \<bottom>)"
   using inv_binf invqka.inv_zero by fastforce
 
-text \<open>We define domain and codomain as in relation algebra and compare with the domain 
+text \<open>We define domain and codomain as in relation algebra and compare with the domain
 and codomain axioms above.\<close>
 
-definition do :: "'a \<Rightarrow> 'a" where 
+definition do :: "'a \<Rightarrow> 'a" where
   "do x = 1 \<sqinter> (x \<cdot> x\<^sup>\<circ>)"
 
 definition cd :: "'a \<Rightarrow> 'a" where
   "cd x = 1 \<sqinter> (x\<^sup>\<circ> \<cdot> x)"
 
 lemma do_inv: "do (x\<^sup>\<circ>) = cd x"
 proof-
   have "do (x\<^sup>\<circ>) = 1 \<sqinter> (x\<^sup>\<circ> \<cdot> (x\<^sup>\<circ>)\<^sup>\<circ>)"
     by (simp add: do_def)
   also have "\<dots> = 1 \<sqinter> (x\<^sup>\<circ> \<cdot> x)"
     by simp
   also have "\<dots> = cd x"
     by (simp add: cd_def)
   finally show ?thesis.
 qed
 
 lemma cd_inv: "cd (x\<^sup>\<circ>) = do x"
   by (simp add: cd_def do_def)
 
 lemma do_le_top: "do x \<le> 1 \<sqinter> (x \<cdot> \<top>)"
   by (simp add: do_def local.inf.coboundedI2 local.mult_isol)
 
 lemma do_subid: "do x \<le> 1"
   by (simp add: do_def)
 
 lemma cd_subid: "cd x \<le> 1"
   by (simp add: cd_def)
 
 lemma do_bot [simp]: "do \<bottom> = \<bottom>"
   by (simp add: do_def)
 
 lemma cd_bot [simp]: "cd \<bottom> = \<bottom>"
   by (simp add: cd_def)
 
 lemma do_iso: "x \<le> y \<Longrightarrow> do x \<le> do y"
   by (simp add: do_def local.inf.coboundedI2 local.inv_iso local.psrpq.mult_isol_var)
 
 lemma cd_iso: "x \<le> y \<Longrightarrow> cd x \<le> cd y"
   using cd_def local.eq_refl local.inf_mono local.inv_iso local.psrpq.mult_isol_var by presburger
 
 lemma do_subdist: "do x \<squnion> do y \<le> do (x \<squnion> y)"
 proof-
   have "do x \<le> do (x \<squnion> y)" and "do y \<le> do (x \<squnion> y)"
     by (simp_all add: do_iso)
   thus ?thesis
     by simp
 qed
 
 lemma cd_subdist: "cd x \<squnion> cd y \<le> cd (x \<squnion> y)"
   by (simp add: cd_iso)
 
 lemma inv_do [simp]: "(do x)\<^sup>\<circ> = do x"
   by (simp add: do_def)
 
 lemma inv_cd [simp]: "(cd x)\<^sup>\<circ> = cd x"
   by (metis do_inv inv_do)
 
 lemma dedekind_modular:
   assumes "(x \<cdot> y) \<sqinter> z \<le> (x \<sqinter> (z \<cdot> y\<^sup>\<circ>)) \<cdot> (y \<sqinter> (x\<^sup>\<circ> \<cdot> z))"
   shows "(x \<cdot> y) \<sqinter> z \<le> (x \<sqinter> (z \<cdot> y\<^sup>\<circ>)) \<cdot> y"
   using assms local.inf.cobounded1 local.mult_isol local.order_trans by blast
 
-lemma modular_eq1: 
+lemma modular_eq1:
   assumes "\<forall>x y z w. (y \<sqinter> (z \<cdot> x\<^sup>\<circ>) \<le> w \<longrightarrow> (y \<cdot> x) \<sqinter> z \<le> w \<cdot> x)"
   shows "\<forall>x y z. (x \<cdot> y) \<sqinter> z \<le> (x \<sqinter> (z \<cdot> y\<^sup>\<circ>)) \<cdot> y"
   using assms by blast
 
 lemma "do x \<cdot> do y = do x \<sqinter> do y" (* nitpick[expect=genuine]*)
   oops
 
 lemma "p \<le> 1 \<Longrightarrow> q \<le> 1 \<Longrightarrow> p \<cdot> q = p \<sqinter> q" (* nitpick[expect=genuine]*)
   oops
 
 end
 
 sublocale ab_unital_quantale \<subseteq> ciq: involutive_quantale id _ _ _ _ _ _ _ _ _ _
   by unfold_locales (simp_all add: mult_commute)
 
 class distributive_involutive_quantale = involutive_quantale + distrib_unital_quantale
 
 class boolean_involutive_quantale = involutive_quantale + bool_unital_quantale
 
 begin
 
-lemma res_peirce: 
+lemma res_peirce:
   assumes "\<forall>x y. x\<^sup>\<circ> \<cdot> -(x \<cdot> y) \<le> -y"
   shows  "((x \<cdot> y) \<sqinter> z\<^sup>\<circ> = \<bottom>) = ((y \<cdot> z) \<sqinter> x\<^sup>\<circ> = \<bottom>)"
 proof
   assume "(x \<cdot> y) \<sqinter> z\<^sup>\<circ> = \<bottom>"
   hence "z\<^sup>\<circ> \<le> -(x \<cdot> y)"
     by (simp add: local.inf.commute local.inf_shunt)
   thus "(y \<cdot> z) \<sqinter> x\<^sup>\<circ> = \<bottom>"
     by (metis assms local.inf_shunt local.inv_conjugate local.inv_contrav local.inv_invol local.mult_isol local.order.trans)
-next 
+next
   assume "(y \<cdot> z) \<sqinter> x\<^sup>\<circ> = \<bottom>"
   hence "x\<^sup>\<circ> \<le> -(y \<cdot> z)"
     using local.compl_le_swap1 local.inf_shunt by blast
   thus "(x \<cdot> y) \<sqinter> z\<^sup>\<circ> = \<bottom>"
     by (metis assms local.dual_order.trans local.inf_shunt local.inv_conjugate local.inv_contrav local.mult_isol)
 qed
 
-lemma res_schroeder1: 
+lemma res_schroeder1:
   assumes "\<forall>x y. x\<^sup>\<circ> \<cdot> -(x \<cdot> y) \<le> -y"
   shows "((x \<cdot> y) \<sqinter> z = \<bottom>) = (y \<sqinter> (x\<^sup>\<circ> \<cdot> z) = \<bottom>)"
 proof
   assume h: "(x \<cdot> y) \<sqinter> z = \<bottom>"
   hence "z \<le> -(x \<cdot> y)"
     by (simp add: local.inf.commute local.inf_shunt)
   thus "y \<sqinter> (x\<^sup>\<circ> \<cdot> z) = \<bottom>"
     by (metis assms local.dual_order.trans local.inf.commute local.inf_shunt local.mult_isol)
-next 
+next
   assume "y \<sqinter> (x\<^sup>\<circ> \<cdot> z) = \<bottom>"
   hence "y \<le> -(x\<^sup>\<circ> \<cdot> z)"
     by (simp add: local.inf_shunt)
   thus "(x \<cdot> y) \<sqinter> z = \<bottom>"
     by (metis assms local.inf_shunt local.inv_invol local.order_trans mult_isol)
 qed
 
-lemma res_schroeder2: 
+lemma res_schroeder2:
   assumes "\<forall>x y. x\<^sup>\<circ> \<cdot> -(x \<cdot> y) \<le> -y"
   shows "((x \<cdot> y) \<sqinter> z = \<bottom>) = (x \<sqinter> (z \<cdot> y\<^sup>\<circ>) = \<bottom>)"
   by (metis assms local.inv_invol local.res_peirce local.res_schroeder1)
 
 lemma res_mod:
   assumes  "\<forall>x y. x\<^sup>\<circ> \<cdot> -(x \<cdot> y) \<le> -y"
   shows "(x \<cdot> y) \<sqinter> z \<le> (x \<sqinter> (z \<cdot> y\<^sup>\<circ>)) \<cdot> y"
 proof-
   have "(x \<cdot> y) \<sqinter> z = ((x \<sqinter> ((z \<cdot> y\<^sup>\<circ>) \<squnion> -(z \<cdot> y\<^sup>\<circ>))) \<cdot> y) \<sqinter> z"
     by simp
   also have "\<dots> = (((x \<sqinter> (z \<cdot> y\<^sup>\<circ>)) \<cdot> y) \<sqinter> z) \<squnion> (((x \<sqinter> -(z \<cdot> y\<^sup>\<circ>)) \<cdot> y) \<sqinter> z)"
     using local.chaq.wswq.distrib_left local.inf.commute local.sup_distr by presburger
   also have "\<dots> \<le> ((x \<sqinter> (z \<cdot> y\<^sup>\<circ>)) \<cdot> y) \<squnion> ((x \<cdot> y) \<sqinter> (-(z \<cdot> y\<^sup>\<circ>)) \<cdot> y \<sqinter> z)"
     by (metis assms local.inf.commute local.inf_compl_bot_right local.sup.orderI local.sup_inf_absorb res_schroeder2)
   also have "\<dots> \<le> ((x \<sqinter> (z \<cdot> y\<^sup>\<circ>)) \<cdot> y) \<squnion> ((x \<cdot> y) \<sqinter> -z  \<sqinter> z)"
     by (metis assms local.dual_order.eq_iff local.inf.commute local.inf_compl_bot_right res_schroeder2)
   also have "\<dots> \<le> ((x \<sqinter> (z \<cdot> y\<^sup>\<circ>)) \<cdot> y)"
     by (simp add: local.inf.commute)
   finally show ?thesis.
 qed
 
 end
 
-text \<open>The strong Gelfand property (name by Palmigiano and Re) is important for dioids and Kleene algebras. 
+text \<open>The strong Gelfand property (name by Palmigiano and Re) is important for dioids and Kleene algebras.
 The modular law is a convenient axiom for relational quantales, in a setting where the underlying
 lattice is not boolean.\<close>
 
 class quantale_converse = involutive_quantale +
   assumes strong_gelfand: "x \<le> x \<cdot> x\<^sup>\<circ> \<cdot> x"
 
 begin
 
 lemma do_gelfand [simp]: "do x \<cdot> do x \<cdot> do x = do x"
   apply (rule order.antisym)
   using local.do_subid local.h_seq local.mult_isol apply fastforce
   by (metis local.inv_do local.strong_gelfand)
- 
+
 lemma cd_gelfand [simp]: "cd x \<cdot> cd x \<cdot> cd x = cd x"
   by (metis do_gelfand local.do_inv)
 
 lemma do_idem [simp]: "do x \<cdot> do x  = do x"
   apply (rule order.antisym)
   using local.do_subid local.mult_isol apply fastforce
   by (metis do_gelfand local.do_subid local.eq_refl local.nsrnqo.mult_oner local.psrpq.mult_isol_var)
 
 lemma cd_idem [simp]: "cd x \<cdot> cd x  = cd x"
   by (metis do_idem local.do_inv)
 
 lemma dodo [simp]: "do (do x) = do x"
 proof-
   have "do (do x) = 1 \<sqinter> (do x \<cdot> do x)"
     using local.do_def local.inv_do by force
   also have "\<dots> = 1 \<sqinter> do x"
     by simp
   also have "\<dots> = do x"
     by (simp add: local.do_def)
   finally show ?thesis.
 qed
 
 lemma cdcd [simp]: "cd (cd x) = cd x"
   using cd_idem local.cd_def local.inv_cd by force
 
 lemma docd_compat [simp]: "do (cd x) = cd x"
 proof-
   have "do (cd x) = do (do (x\<^sup>\<circ>))"
     by (simp add: local.do_inv)
   also have "\<dots> = do (x\<^sup>\<circ>)"
     by simp
   also have "\<dots> = cd x"
     by (simp add: local.do_inv)
   finally show ?thesis.
 qed
 
 lemma cddo_compat [simp]: "cd (do x) = do x"
   by (metis docd_compat local.cd_inv local.inv_do)
 
 end
 
 sublocale quantale_converse \<subseteq> convqka: kleene_algebra_converse "(\<squnion>)" "(\<cdot>)" 1 \<bottom> "(\<le>)" "(<)" invol qstar
   by unfold_locales (simp add: local.strong_gelfand)
 
 
 subsection \<open>Dedekind quantales\<close>
 
 class dedekind_quantale = involutive_quantale +
   assumes modular_law: "(x \<cdot> y) \<sqinter> z \<le> (x \<sqinter> (z \<cdot> y\<^sup>\<circ>)) \<cdot> y"
 
 begin
 
 sublocale convdqka: kleene_algebra_converse  "(\<squnion>)" "(\<cdot>)" 1 \<bottom> "(\<le>)" "(<)" invol qstar
   by unfold_locales (metis local.inf.absorb2 local.le_top local.modular_law local.top_greatest)
 
 subclass quantale_converse
   by unfold_locales (simp add: local.convdqka.strong_gelfand)
 
 lemma modular_2 [simp]: "((x \<sqinter> (z \<cdot> y\<^sup>\<circ>)) \<cdot> y) \<sqinter> z = (x \<cdot> y) \<sqinter> z"
   apply (rule order.antisym)
   using local.inf.cobounded1 local.inf_mono local.mult_isor local.order_refl apply presburger
   by (simp add: local.modular_law)
 
 lemma modular_1 [simp]: "(x \<cdot> (y \<sqinter> (x\<^sup>\<circ> \<cdot> z))) \<sqinter> z = (x \<cdot> y) \<sqinter> z"
   by (metis local.inv_binf local.inv_contrav local.inv_invol modular_2)
 
 lemma modular3: "(x \<cdot> y) \<sqinter> z \<le> x \<cdot> (y \<sqinter> (x\<^sup>\<circ> \<cdot> z))"
   by (metis local.inf.cobounded1 modular_1)
 
 text \<open>The name Dedekind quantale owes to the following formula, which is equivalent to the modular law. Dedekind quantales
-are called modular quantales in Rosenthal's book on quantaloids (to be precise: he discusses modular quantaloids, but the 
+are called modular quantales in Rosenthal's book on quantaloids (to be precise: he discusses modular quantaloids, but the
 notion of modular quantale is then obvious).\<close>
 
 lemma dedekind: "(x \<cdot> y) \<sqinter> z \<le> (x \<sqinter> (z \<cdot> y\<^sup>\<circ>)) \<cdot> (y \<sqinter> (x\<^sup>\<circ> \<cdot> z))"
 proof-
   have  "(x \<cdot> y) \<sqinter> z = (x \<cdot> (y \<sqinter> (x\<^sup>\<circ> \<cdot> z))) \<sqinter> z"
     by simp
   also have "\<dots> \<le> (x \<sqinter> (z \<cdot> (y \<sqinter> (x\<^sup>\<circ> \<cdot> z))\<^sup>\<circ>)) \<cdot> (y \<sqinter> (x\<^sup>\<circ> \<cdot> z))"
     using local.modular_law by presburger
   also have "\<dots> = (x \<sqinter> (z \<cdot> (y\<^sup>\<circ> \<sqinter> (z\<^sup>\<circ> \<cdot> x)))) \<cdot> (y \<sqinter> (x\<^sup>\<circ> \<cdot> z))"
     by simp
   also have "\<dots> \<le> (x \<sqinter> (z \<cdot> y\<^sup>\<circ>)) \<cdot> (y \<sqinter> (x\<^sup>\<circ> \<cdot> z))"
     using local.inf.commute modular_1 by fastforce
   finally show ?thesis.
 qed
 
 lemma peirce: "((x \<cdot> y) \<sqinter> z\<^sup>\<circ> = \<bottom>) = ((y \<cdot> z) \<sqinter> x\<^sup>\<circ> = \<bottom>)"
 proof
   assume "(x \<cdot> y) \<sqinter> z\<^sup>\<circ> = \<bottom>"
   hence "((x \<cdot> y) \<sqinter> z\<^sup>\<circ>) \<cdot> y\<^sup>\<circ> = \<bottom>"
     by simp
   hence "(z\<^sup>\<circ> \<cdot> y\<^sup>\<circ>) \<sqinter> x = \<bottom>"
     by (metis local.inf.commute local.inv_invol local.le_bot local.modular_law)
   hence "((y \<cdot> z) \<sqinter> x\<^sup>\<circ>)\<^sup>\<circ> = \<bottom>\<^sup>\<circ>"
     by simp
   thus "(y \<cdot> z) \<sqinter> x\<^sup>\<circ> = \<bottom>"
     by (metis local.inv_invol)
 next
   assume h: "(y \<cdot> z) \<sqinter> x\<^sup>\<circ> = \<bottom>"
   hence "z\<^sup>\<circ> \<cdot> ((y \<cdot> z) \<sqinter> x\<^sup>\<circ>) = \<bottom>"
     by simp
   hence "(y\<^sup>\<circ> \<cdot> x\<^sup>\<circ>) \<sqinter> z = \<bottom>"
     by (metis h local.inf.commute local.inv_invol local.le_bot local.mult_botr modular3)
    hence "((x \<cdot> y) \<sqinter> z\<^sup>\<circ>)\<^sup>\<circ> = \<bottom>\<^sup>\<circ>"
     by simp
   thus "(x \<cdot> y) \<sqinter> z\<^sup>\<circ> = \<bottom>"
     by (metis local.inv_invol)
 qed
 
 lemma schroeder_1: "((x \<cdot> y) \<sqinter> z = \<bottom>) = (y \<sqinter> (x\<^sup>\<circ> \<cdot> z) = \<bottom>)"
   by (metis local.inf.commute local.inf_bot_right local.inv_invol local.mult_botr modular_1)
 
 lemma schroeder_2: "((x \<cdot> y) \<sqinter> z = \<bottom>) = (x \<sqinter> (z \<cdot> y\<^sup>\<circ>) = \<bottom>)"
   by (metis local.inv_invol peirce schroeder_1)
 
 lemma modular_eq2: "y \<sqinter> (z \<cdot> x\<^sup>\<circ>) \<le> w \<Longrightarrow> (y \<cdot> x) \<sqinter> z \<le> w \<cdot> x"
   by (meson local.dual_order.trans local.eq_refl local.h_w1 local.modular_law)
 
 lemma lla_top_aux: "p \<le> 1 \<Longrightarrow> ((x \<le> p \<cdot> x) = (x \<le> p \<cdot> \<top>))"
 proof
   assume h: "p \<le> 1"
   and h1: "x \<le> p \<cdot> x"
   thus "x \<le> p \<cdot> \<top>"
     by (meson local.mult_isol local.order_trans local.top_greatest)
-next 
+next
   assume h: "p \<le> 1"
   and "x \<le> p \<cdot> \<top>"
   hence "x = (p \<cdot> \<top>) \<sqinter> x"
     using local.inf.absorb_iff2 by auto
   also have "\<dots> \<le> p \<cdot> (\<top> \<sqinter> (p\<^sup>\<circ> \<cdot> x))"
     using modular3 by blast
   also have "\<dots> = p \<cdot> p \<cdot> x"
     by (simp add: h local.convdqka.subid_conv mult_assoc)
   finally show "x \<le> p \<cdot> x"
     by (metis h local.dual_order.trans local.mult_isor local.nsrnqo.mult_onel)
 qed
 
 text \<open>Next we turn to properties of domain and codomain in Dedekind quantales.\<close>
 
 lemma lra_top_aux: "p \<le> 1 \<Longrightarrow> ((x \<le> x \<cdot> p ) = (x \<le> \<top> \<cdot> p))"
   by (metis convdqka.subid_conv local.inf.absorb_iff2 local.mult_1_right local.psrpq.subdistl local.sup.absorb_iff2 local.top_greatest modular_eq2)
 
 lemma lla: "p \<le> 1 \<Longrightarrow> ((do x \<le> p) = (x \<le> p \<cdot> \<top>))"
-proof 
+proof
   assume a1: "x \<le> p \<cdot> \<top>"
   assume a2: "p \<le> 1"
   have f3: "x \<cdot> \<top> \<le> p \<cdot> \<top> \<cdot> \<top>"
     by (simp add: a1 local.mult_isor)
   have f4: "p \<cdot> do x \<le> p"
     by (simp add: local.do_subid local.uqka.star_inductr_var_equiv local.uwqlka.star_subid)
   have "x \<cdot> \<top> \<le> p \<cdot> \<top>"
     using f3 by (simp add: local.mult.semigroup_axioms semigroup.assoc)
   thus "do x \<le> p"
     using f4 a2 lla_top_aux local.do_le_top local.inf.bounded_iff local.order_trans by blast
-next 
+next
   assume a1: "do x \<le> p"
   assume a2: "p \<le> 1"
   hence  "do x \<cdot> x \<le> p \<cdot> x"
     by (simp add: a1 local.mult_isor)
   hence "x \<le> p \<cdot> x"
     using a1 local.do_def modular_eq2 by fastforce
   thus "x \<le> p \<cdot> \<top>"
     by (simp add: a2 lla_top_aux)
 qed
 
 lemma lla_Inf: "do x = \<Sqinter>{p. x \<le> p \<cdot> \<top> \<and> p \<le> 1}"
   apply (rule order.antisym)
   using lla local.Inf_greatest apply fastforce
   by (metis CollectI lla local.Inf_lower local.do_subid local.order.refl)
 
 lemma lra: "p \<le> 1 \<Longrightarrow> ((cd x \<le> p) = (x \<le> \<top> \<cdot> p))"
   by (metis invqka.inv_adj lla local.convdqka.subid_conv local.do_inv local.inv_contrav local.inv_top)
 
 lemma lra_Inf: "cd x = \<Sqinter>{p. x \<le> \<top> \<cdot> p \<and> p \<le> 1}"
   apply (rule order.antisym)
   using local.Inf_greatest lra apply fastforce
   by (metis CollectI local.Inf_lower local.cd_subid local.order.refl lra)
 
 lemma lla_var: "p \<le> 1 \<Longrightarrow> ((do x \<le> p) = (x \<le> p \<cdot> x))"
   by (simp add: lla lla_top_aux)
 
 lemma lla_Inf_var: "do x = \<Sqinter>{p. x \<le> p \<cdot> x \<and> p \<le> 1}"
   apply (rule order.antisym)
   using lla_var local.Inf_greatest apply fastforce
   by (metis CollectI lla_var local.Inf_lower local.do_subid local.order.refl)
 
 lemma lra_var: "p \<le> 1 \<Longrightarrow> ((cd x \<le> p) = (x \<le> x \<cdot> p))"
   by (simp add: lra lra_top_aux)
 
 lemma lra_Inf_var: "cd x = \<Sqinter>{p. x \<le> x \<cdot> p \<and> p \<le> 1}"
   apply (rule order.antisym)
   using local.Inf_greatest lra_var apply fastforce
   by (metis CollectI local.Inf_lower local.cd_subid local.order.refl lra_var)
 
 lemma do_top: "do x = 1 \<sqinter> (x \<cdot> \<top>)"
 proof-
   have "1 \<sqinter> (x \<cdot> \<top>) = 1 \<sqinter> (x \<cdot> (\<top> \<sqinter> x\<^sup>\<circ> \<cdot> 1))"
     by (metis local.inf.commute local.inf_top.left_neutral modular_1)
   also have "\<dots> = do x"
     by (simp add: local.do_def)
   finally show ?thesis..
 qed
 
 lemma cd_top: "cd x = 1 \<sqinter> (\<top> \<cdot> x)"
   by (metis do_top invqka.inv_one local.do_inv local.inv_binf local.inv_cd local.inv_contrav local.inv_invol local.inv_top)
 
 text \<open>We start deriving the axioms of modal semirings and modal quantales.\<close>
 
 lemma do_absorp: "x \<le> do x \<cdot> x"
   using lla_var local.do_subid by blast
 
 lemma cd_absorp: "x \<le> x \<cdot> cd x"
   using local.cd_subid lra_var by blast
 
 lemma do_absorp_eq [simp]: "do x \<cdot> x = x"
   using do_absorp local.do_subid local.dual_order.antisym local.h_w1 by fastforce
 
 lemma cd_absorp_eq [simp]: "x \<cdot> cd x = x"
   by (metis do_top local.do_inv local.inf_top.right_neutral local.nsrnqo.mult_oner modular_1)
 
 lemma do_top2: "x \<cdot> \<top> = do x \<cdot> \<top>"
 proof (rule order.antisym)
   have "x \<cdot> \<top> = do x \<cdot> x \<cdot> \<top>"
     by simp
   also have "\<dots> \<le> do x \<cdot> \<top> \<cdot> \<top>"
     using local.psrpq.mult_double_iso local.top_greatest by presburger
   also have "\<dots> = do x \<cdot> \<top>"
     by (simp add: local.mult.semigroup_axioms semigroup.assoc)
   finally show "x \<cdot> \<top> \<le> do x \<cdot> \<top>".
   have "do x \<cdot> \<top> = (1 \<sqinter> (x \<cdot> \<top>)) \<cdot> \<top>"
     by (simp add: do_top)
   also have "\<dots> \<le> (1 \<cdot> \<top>) \<sqinter> (x \<cdot> \<top> \<cdot> \<top>)"
     by (simp add: local.mult_isor)
   also have "\<dots> = x \<cdot> \<top>"
     by (simp add: mult_assoc)
   finally show "do x \<cdot> \<top> \<le> x \<cdot> \<top>".
 qed
 
 lemma cd_top2: "\<top> \<cdot> x  = \<top> \<cdot> cd x"
   by (metis do_top2 local.do_inv local.inv_cd local.inv_contrav local.inv_invol local.inv_top)
 
 lemma do_local [simp]: "do (x \<cdot> do y) = do (x \<cdot> y)"
 proof-
   have "do (x \<cdot> do y) = 1 \<sqinter> (x \<cdot> do y \<cdot> \<top>)"
     using do_top by force
   also have "\<dots> = 1 \<sqinter> (x \<cdot> y \<cdot> \<top>)"
     using do_top2 mult_assoc by force
   also have "\<dots> = do (x \<cdot> y)"
     by (simp add: do_top)
   finally show ?thesis
     by force
 qed
 
 lemma cd_local [simp]: "cd (cd x \<cdot> y) = cd (x \<cdot> y)"
   by (metis cd_top cd_top2 mult_assoc)
 
 lemma do_fix_subid: "(do x = x) = (x \<le> 1)"
 proof
   assume "do x = x"
   thus "x \<le> 1"
     by (metis local.do_subid)
-next 
+next
   assume a: "x \<le> 1"
   hence "x = do x \<cdot> x"
     by simp
   hence b: "x \<le> do x"
     by (metis a local.mult_isol local.nsrnqo.mult_oner)
   have "x \<cdot> x \<le> x"
     using a local.mult_isor by fastforce
   hence  "do x \<le> x"
     by (simp add: a lla_var local.le_top lra_top_aux)
   thus "do x = x"
     by (simp add: b local.dual_order.antisym)
 qed
 
 lemma cd_fix_subid: "(cd x = x) = (x \<le> 1)"
   by (metis local.convdqka.subid_conv local.do_inv local.do_fix_subid local.docd_compat)
 
 lemma do_inf2: "do (do x \<sqinter> do y) = do x \<sqinter> do y"
   using do_top local.do_fix_subid local.inf.assoc by auto
 
 lemma do_inf_comp: "do x \<cdot> do y = do x \<sqinter> do y"
   by (smt (verit, best) local.do_def local.do_idem local.do_fix_subid local.dodo local.dual_order.trans local.inf_commute local.inf_idem local.inv_contrav local.inv_do local.mult_1_right local.mult_isol modular_1 mult_assoc)
 
 lemma cd_inf_comp: "cd x \<cdot> cd y = cd x \<sqinter> cd y"
   by (metis do_inf_comp local.docd_compat)
 
 lemma subid_mult_meet: "p \<le> 1 \<Longrightarrow> q \<le> 1 \<Longrightarrow> p \<cdot> q = p \<sqinter> q"
   by (metis do_inf_comp local.do_fix_subid)
 
 lemma dodo_sup: "do (do x \<squnion> do y) = do x \<squnion> do y"
 proof-
   have "do (do x \<squnion> do y) = 1 \<sqinter> ((do x \<squnion> do y) \<cdot> (do x \<squnion> do y)\<^sup>\<circ>)"
     using local.do_def by blast
   also have "\<dots> = 1 \<sqinter> ((do x \<squnion> do y) \<cdot> (do x \<squnion> do y))"
     by simp
   also have "\<dots> = 1 \<sqinter> (do x \<squnion> do y)"
     using local.do_subid local.dodo local.inf.idem local.le_supI subid_mult_meet by presburger
   also have "\<dots> = do x \<squnion> do y"
     by (simp add: local.do_def local.inf_absorb2)
   finally show ?thesis.
 qed
 
 lemma do_sup [simp]: "do (x \<squnion> y) = do x \<squnion> do y"
 proof-
   have "do (x \<squnion> y) = 1 \<sqinter> ((x \<squnion> y) \<cdot> \<top>)"
     by (simp add: do_top)
   also have "\<dots> = 1 \<sqinter> (x \<cdot> \<top> \<squnion> y \<cdot> \<top>)"
     by simp
   also have "\<dots> = 1 \<sqinter> (do x \<cdot> \<top> \<squnion> do y \<cdot> \<top>)"
     using do_top2 by force
   also have "\<dots> = 1 \<sqinter> ((do x \<squnion> do y) \<cdot> \<top>)"
     by simp
   also have "\<dots> = do (do x \<squnion> do y)"
     by (simp add: do_top)
   finally show ?thesis
     by (simp add: dodo_sup)
 qed
 
 lemma cdcd_sup: "cd (cd x \<squnion> cd y) = cd x \<squnion> cd y"
   using local.cd_fix_subid by fastforce
 
 lemma cd_sup [simp]: "cd (x \<squnion> y) = cd x \<squnion> cd y"
   by (metis do_sup local.do_inv local.inv_binsup)
 
 text \<open>Next we show that Dedekind quantales are modal quantales, hence also modal semirings.\<close>
 
 sublocale dmq: dc_modal_quantale 1 "(\<cdot>)" Inf Sup "(\<sqinter>)" "(\<le>)" "(<)" "(\<squnion>)" "\<bottom>" "\<top>" cd do
 proof
   show "\<And>x. cd x \<le> 1"
     by (simp add: cd_top)
   show "\<And>x. do x \<le> 1"
     by (simp add: do_top)
 qed simp_all
 
 lemma do_top3 [simp]: "do (x \<cdot> \<top>) = do x"
   using dmq.coddual.le_top dmq.dqmsr.domain_1'' local.do_iso local.order.antisym by presburger
 
 lemma cd_top3 [simp]: "cd (\<top> \<cdot> x) = cd x"
   by (simp add: cd_top dmq.coddual.mult_assoc)
 
 lemma dodo_Sup_pres: "do (\<Squnion>x \<in> X. do x) = (\<Squnion>x \<in> X. do x)"
   by (simp add: local.SUP_least local.do_fix_subid)
 
 text \<open>The domain elements form a complete Heyting algebra.\<close>
 
 lemma do_complete_heyting: "do x \<sqinter> (\<Squnion>y \<in> Y. do y) = (\<Squnion>y \<in> Y. do x \<sqinter> do y)"
 proof-
   have "do x \<sqinter> (\<Squnion>y \<in> Y. do y) = do x \<cdot> (\<Squnion>y \<in> Y. do y)"
     by (metis do_inf_comp dodo_Sup_pres)
   also have "\<dots> = (\<Squnion>y \<in> Y. do x \<cdot> do y)"
     by (simp add: dmq.coddual.Sup_distr image_image)
   also have "\<dots> = (\<Squnion>y \<in> Y. do x \<sqinter> do y)"
     using do_inf_comp by force
   finally show ?thesis.
 qed
 
 lemma cdcd_Sup_pres: "cd (\<Squnion>x \<in> X. cd x) = (\<Squnion>x \<in> X. cd x)"
   by (simp add: local.SUP_least local.cd_fix_subid)
 
 lemma cd_complete_heyting: "cd x \<sqinter> (\<Squnion>y \<in> Y. cd y) = (\<Squnion>y \<in> Y. cd x \<sqinter> cd y)"
 proof-
   have "cd x \<sqinter> (\<Squnion>y \<in> Y. cd y) = cd x \<cdot> (\<Squnion>y \<in> Y. cd y)"
     by (metis cd_inf_comp cdcd_Sup_pres)
   also have "\<dots> = (\<Squnion>y \<in> Y. cd x \<cdot> cd y)"
     by (simp add: dmq.coddual.Sup_distr image_image)
   also have "\<dots> = (\<Squnion>y \<in> Y. cd x \<sqinter> cd y)"
     using cd_inf_comp by force
   finally show ?thesis.
 qed
 
-lemma subid_complete_heyting: 
+lemma subid_complete_heyting:
   assumes "p \<le> 1"
   and "\<forall>q \<in> Q. q \<le> 1"
   shows "p \<sqinter> (\<Squnion>Q) = (\<Squnion>q \<in> Q. p \<sqinter> q)"
 proof-
   have a: "do p = p"
     by (simp add: assms(1) local.do_fix_subid)
   have b: "\<forall>q \<in> Q. do q = q"
     using assms(2) local.do_fix_subid by presburger
   hence "p \<sqinter> (\<Squnion>Q) = do p \<sqinter> (\<Squnion>q \<in> Q. do q)"
     by (simp add: a)
   also have "\<dots> = (\<Squnion>q \<in> Q. do p \<sqinter> do q)"
     using do_complete_heyting by blast
   also have "\<dots> = (\<Squnion>q \<in> Q. p \<sqinter> q)"
     using a b by force
   finally show ?thesis.
 qed
 
 text \<open>Next we show that domain and codomain preserve arbitrary Sups.\<close>
 
 lemma do_Sup_pres_aux: "(\<Squnion>x \<in> X. do x \<cdot> \<top>) = (\<Squnion>x \<in> do ` X. x \<cdot> \<top>)"
   by (smt (verit, best) Sup.SUP_cong image_image)
 
 lemma do_Sup_pres: "do (\<Squnion>x \<in> X. x) = (\<Squnion>x \<in> X. do x)"
 proof-
   have "do (\<Squnion>x \<in> X. x) = 1 \<sqinter> ((\<Squnion>x \<in> X. x) \<cdot> \<top>)"
     by (simp add: do_top)
   also have "\<dots> = 1 \<sqinter> (\<Squnion>x \<in> X. x \<cdot> \<top>)"
     by (simp add: dmq.coddual.Sup_distl)
   also have "\<dots> = 1 \<sqinter> (\<Squnion>x \<in> X. do x \<cdot> \<top>)"
     using do_top2 by force
   also have "\<dots> = 1 \<sqinter> (\<Squnion>x \<in> do ` X. x \<cdot> \<top>)"
     using do_Sup_pres_aux by presburger
   also have "\<dots> = 1 \<sqinter> ((\<Squnion>x \<in> X. do x) \<cdot> \<top>)"
     using dmq.coddual.Sup_distl by presburger
   also have "\<dots> = do (\<Squnion>x \<in> X. do x)"
     by (simp add: do_top)
   finally show ?thesis
     using dodo_Sup_pres by presburger
 qed
 
 lemma cd_Sup_pres: "cd (\<Squnion>x \<in> X. x) = (\<Squnion>x \<in> X. cd x)"
 proof-
   have "cd (\<Squnion>x \<in> X. x) = do ((\<Squnion>x \<in> X. x)\<^sup>\<circ>)"
     using local.do_inv by presburger
   also have "\<dots> = do (\<Squnion>x \<in> X. x\<^sup>\<circ>)"
     by simp
   also have "\<dots> = (\<Squnion>x \<in> X. do (x\<^sup>\<circ>))"
     by (metis do_Sup_pres image_ident image_image)
   also have "\<dots> = (\<Squnion>x \<in> X. cd x)"
     using local.do_inv by presburger
   finally show ?thesis.
 qed
 
 lemma do_inf: "do (x \<sqinter> y) = 1 \<sqinter> (y \<cdot> x\<^sup>\<circ>)"
   by (smt (z3) do_absorp_eq invqka.inv_one local.do_def local.inf_commute local.inv_binf local.inv_contrav local.inv_invol local.mult_1_right modular_1 modular_2 mult_assoc)
 
 lemma cd_inf: "cd (x \<sqinter> y) = 1 \<sqinter> (y\<^sup>\<circ> \<cdot> x)"
   by (metis do_inf local.do_inv local.inv_binf local.inv_invol)
 
 lemma do_bres_prop: "p \<le> 1 \<Longrightarrow> do (x \<rightarrow> p \<cdot> \<top>) = 1 \<sqinter> (x \<rightarrow> p \<cdot> \<top>)"
   by (simp add: do_top)
 
 lemma cd_fres_prop: "p \<le> 1 \<Longrightarrow> cd (\<top> \<cdot> p \<leftarrow> x) = 1 \<sqinter> (\<top> \<cdot> p \<leftarrow> x)"
   by (simp add: cd_top)
 
 lemma do_meet_prop: "(do p \<cdot> x) \<sqinter> (x \<cdot> do q) = do p \<cdot> x \<cdot> do q"
 proof (rule order.antisym)
   have "x \<sqinter> (do p \<cdot> x \<cdot> do q) \<le> do p \<cdot> x"
     by (simp add: dmq.dqmsr.dom_subid_aux2'' local.inf.coboundedI2)
   thus  "(do p \<cdot> x) \<sqinter> (x \<cdot> do q) \<le> do p \<cdot> x \<cdot> do q"
     by (simp add: local.inf.commute modular_eq2)
 next
   have "do p \<cdot> x \<cdot> do q = (do p \<cdot> x \<cdot> do q) \<sqinter> (do p \<cdot> x \<cdot> do q)"
     by simp
   also have "\<dots> \<le> (do p \<cdot> x) \<sqinter> (x \<cdot> do q)"
     using dmq.dqmsr.dom_subid_aux2 dmq.dqmsr.dom_subid_aux2'' local.psrpq.mult_isol_var by auto
   finally show "do p \<cdot> x \<cdot> do q \<le> (do p \<cdot> x) \<sqinter> (x \<cdot> do q)".
 qed
 
 lemma subid_meet_prop: "p \<le> 1 \<Longrightarrow> q \<le> 1 \<Longrightarrow> (p \<cdot> x) \<sqinter> (x \<cdot> q) = p \<cdot> x \<cdot> q"
   by (metis do_fix_subid do_meet_prop)
 
-text \<open>Next we consider box and diamond operators like in modal semirings and modal quantales. 
-These are inherited from domain quantales. Diamonds are defined with respect to domain and codomain. 
+text \<open>Next we consider box and diamond operators like in modal semirings and modal quantales.
+These are inherited from domain quantales. Diamonds are defined with respect to domain and codomain.
 The box operators are defined as Sups and hence right adjoints of diamonds.\<close>
 
 abbreviation "do_dia \<equiv> dmq.fd'"
 
 abbreviation "cd_dia \<equiv> dmq.bd'"
 
 abbreviation "do_box \<equiv> dmq.bb"
 
 abbreviation "cd_box \<equiv> dmq.fb"
 
 text \<open>In the sense of modal logic, the domain-based diamond is a backward operator, the codomain-based
 one a forward operator. These are related by opposition/converse.\<close>
 
 lemma do_dia_cd_dia_conv: "p \<le> 1 \<Longrightarrow> do_dia (x\<^sup>\<circ>) p = cd_dia x p"
   by (simp add: convdqka.subid_conv dmq.coddual.dqmsr.fd_def dmq.dqmsr.fd_def local.cd_def local.do_def)
 
 lemma cd_dia_do_dia_conv: "p \<le> 1 \<Longrightarrow> cd_dia (x\<^sup>\<circ>) p = do_dia x p"
   by (metis do_dia_cd_dia_conv local.inv_invol)
 
 text \<open>Diamonds preserve sups in both arguments.\<close>
 
 lemma do_dia_Sup: "do_dia (\<Squnion>X) p = (\<Squnion>x \<in> X. do_dia x p)"
 proof-
   have "do_dia (\<Squnion>X) p = do ((\<Squnion>X) \<cdot> p)"
     by (simp add: dmq.dqmsr.fd_def)
   also have "\<dots> = do (\<Squnion>x \<in> X. x \<cdot> p)"
     using local.Sup_distr by fastforce
  also have "\<dots> = (\<Squnion>x \<in> X. do (x \<cdot> p))"
    by (metis do_Sup_pres image_ident image_image)
   also have "\<dots> = (\<Squnion>x \<in> X. do_dia x p)"
     using dmq.dqmsr.fd_def by fastforce
   finally show ?thesis.
 qed
 
 lemma do_dia_Sup2: "do_dia x (\<Squnion>P) = (\<Squnion>p \<in> P. do_dia x p)"
 proof-
   have  "do_dia x (\<Squnion>P) = do (x \<cdot> (\<Squnion>P))"
     by (simp add: dmq.dqmsr.fd_def)
   also have "\<dots> = (\<Squnion>p \<in> P. do (x \<cdot> p))"
     by (metis dmq.coddual.Sup_distr do_Sup_pres image_ident image_image)
   also have "\<dots> = (\<Squnion>p \<in> P. do_dia x p)"
     using dmq.dqmsr.fd_def by auto
   finally show ?thesis.
 qed
 
 lemma cd_dia_Sup: "cd_dia (\<Squnion>X) p = (\<Squnion>x \<in> X. cd_dia x p)"
 proof-
   have "cd_dia (\<Squnion>X) p = cd (p \<cdot> (\<Squnion>X))"
     by (simp add: dmq.coddual.dqmsr.fd_def)
   also have "\<dots> = cd (\<Squnion>x \<in> X. p \<cdot> x)"
     using dmq.coddual.Sup_distr by auto
  also have "\<dots> = (\<Squnion>x \<in> X. cd (p \<cdot> x))"
    by (metis cd_Sup_pres image_ident image_image)
   also have "\<dots> = (\<Squnion>x \<in> X. cd_dia x p)"
     using dmq.coddual.dqmsr.fd_def by force
   finally show ?thesis.
 qed
 
 lemma cd_dia_Sup2: "cd_dia x (\<Squnion>P) = (\<Squnion>p \<in> P. cd_dia x p)"
 proof-
   have  "cd_dia x (\<Squnion>P) = cd ((\<Squnion>P) \<cdot> x)"
     by (simp add: dmq.coddual.dqmsr.fd_def)
   also have "\<dots> = (\<Squnion>p \<in> P. cd (p \<cdot> x))"
     by (metis cd_Sup_pres dmq.coddual.Sup_distl image_ident image_image)
   also have "\<dots> = (\<Squnion>p \<in> P. cd_dia x p)"
     using dmq.coddual.dqmsr.fd_def by auto
   finally show ?thesis.
 qed
 
 text \<open>The domain-based box is a forward operator, the codomain-based on a backward one. These interact
 again with respect to converse.\<close>
 
 lemma do_box_var: "p \<le> 1 \<Longrightarrow> do_box x p = \<Squnion>{q. do_dia x q \<le> p \<and> q \<le> 1}"
   by (smt (verit, best) Collect_cong dmq.bb_def dmq.dqmsr.fdia_d_simp local.do_fix_subid local.dodo)
 
 lemma cd_box_var: "p \<le> 1 \<Longrightarrow> cd_box x p = \<Squnion>{q. cd_dia x q \<le> p \<and> q \<le> 1}"
   by (smt (verit, best) Collect_cong dmq.coddual.dqmsr.fdia_d_simp dmq.fb_def local.cd_fix_subid local.cdcd)
 
 lemma do_box_cd_box_conv: "p \<le> 1 \<Longrightarrow> do_box (x\<^sup>\<circ>) p = cd_box x p"
 proof-
   assume a: "p \<le> 1"
   hence "do_box (x\<^sup>\<circ>) p = \<Squnion>{q. do_dia (x\<^sup>\<circ>) q \<le> p \<and> q \<le> 1}"
     by (simp add: do_box_var)
   also have "\<dots> =  \<Squnion>{q. cd_dia x q \<le> p \<and> q \<le> 1}"
     by (metis do_dia_cd_dia_conv)
   also have "\<dots> = cd_box x p"
     using a cd_box_var by auto
   finally show ?thesis.
 qed
 
 lemma cd_box_do_box_conv: "p \<le> 1 \<Longrightarrow> cd_box (x\<^sup>\<circ>) p = do_box x p"
   by (metis do_box_cd_box_conv local.inv_invol)
 
 lemma do_box_subid: "do_box x p \<le> 1"
   using dmq.bb_def local.Sup_le_iff by force
 
 lemma cd_box_subid: "p \<le> 1 \<Longrightarrow> cd_box x p \<le> 1"
   by (metis do_box_subid local.do_box_cd_box_conv)
 
-text \<open>Next we prove that boxes and diamonds are adjoints, and then demodalisation laws known 
+text \<open>Next we prove that boxes and diamonds are adjoints, and then demodalisation laws known
 from modal semirings.\<close>
 
-lemma do_dia_do_box_galois: 
+lemma do_dia_do_box_galois:
   assumes "p \<le> 1"
-  and "q \<le> 1" 
+  and "q \<le> 1"
   shows "(do_dia x p \<le> q) = (p \<le> do_box x q)"
 proof
   show "do_dia x p \<le> q \<Longrightarrow> p \<le> do_box x q"
     by (simp add: assms do_box_var local.Sup_upper)
 next
   assume "p \<le> do_box x q"
   hence "do_dia x p \<le> do (x \<cdot> \<Squnion>{t. do_dia x t \<le> q \<and> t \<le> 1})"
     by (simp add: assms(2) local.dmq.dqmsr.fd_def local.do_box_var local.do_iso local.mult_isol)
   also have "\<dots> = \<Squnion>{do (x \<cdot> t) |t. do_dia x t \<le> q \<and> t \<le> 1}"
     by (metis do_Sup_pres image_ident image_image local.Sup_distl setcompr_eq_image)
   also have "\<dots> = \<Squnion>{do_dia x t |t. do_dia x t \<le> q \<and> t \<le> 1}"
     using local.dmq.dqmsr.fd_def by fastforce
   also have "\<dots> \<le> q"
     using local.Sup_le_iff by blast
   finally have "do_dia x p \<le> q".
   thus "p \<le> do_box x q \<Longrightarrow> do_dia x p \<le> q".
 qed
 
-lemma cd_dia_cd_box_galois: 
+lemma cd_dia_cd_box_galois:
   assumes "p \<le> 1"
   and "q \<le> 1"
 shows "(cd_dia x p \<le> q) = (p \<le> cd_box x q)"
   by (metis assms do_box_cd_box_conv do_dia_cd_dia_conv do_dia_do_box_galois)
 
-lemma do_dia_demod_subid: 
-  assumes "p \<le> 1" 
+lemma do_dia_demod_subid:
+  assumes "p \<le> 1"
   and "q \<le> 1"
 shows "(do_dia x p \<le> q) = (x \<cdot> p \<le> q \<cdot> x)"
   by (metis assms dmq.dqmsr.fdemodalisation2 local.do_fix_subid)
 
 text \<open>The demodalisation laws have variants based on residuals.\<close>
 
-lemma do_dia_demod_subid_fres: 
-  assumes "p \<le> 1" 
+lemma do_dia_demod_subid_fres:
+  assumes "p \<le> 1"
   and "q \<le> 1"
   shows "(do_dia x p \<le> q) = (p \<le> x \<rightarrow> q \<cdot> x)"
   by (simp add: assms do_dia_demod_subid local.bres_galois)
 
-lemma do_dia_demod_subid_var: 
-  assumes "p \<le> 1" 
+lemma do_dia_demod_subid_var:
+  assumes "p \<le> 1"
   and "q \<le> 1"
 shows "(do_dia x p \<le> q) = (x \<cdot> p \<le> q \<cdot> \<top>)"
   by (simp add: assms(2) dmq.dqmsr.fd_def lla)
 
-lemma do_dia_demod_subid_var_fres: 
-  assumes "p \<le> 1" 
+lemma do_dia_demod_subid_var_fres:
+  assumes "p \<le> 1"
   and "q \<le> 1"
 shows "(do_dia x p \<le> q) = (p \<le> x \<rightarrow> q \<cdot> \<top>)"
   by (simp add: assms do_dia_demod_subid_var local.bres_galois)
 
-lemma cd_dia_demod_subid: 
-  assumes "p \<le> 1" 
+lemma cd_dia_demod_subid:
+  assumes "p \<le> 1"
   and "q \<le> 1"
 shows "(cd_dia x p \<le> q) = (p \<cdot> x \<le> x \<cdot> q)"
   by (metis assms dmq.coddual.dqmsr.fdemodalisation2 local.cd_fix_subid)
 
-lemma cd_dia_demod_subid_fres: 
-  assumes "p \<le> 1" 
+lemma cd_dia_demod_subid_fres:
+  assumes "p \<le> 1"
   and "q \<le> 1"
 shows "(cd_dia x p \<le> q) = (p \<le> x \<cdot> q \<leftarrow> x)"
   by (simp add: assms cd_dia_demod_subid local.fres_galois)
 
-lemma cd_dia_demod_subid_var: 
-  assumes "p \<le> 1" 
+lemma cd_dia_demod_subid_var:
+  assumes "p \<le> 1"
   and "q \<le> 1"
 shows "(cd_dia x p \<le> q) = (p \<cdot> x \<le> \<top> \<cdot> q)"
   by (simp add: assms(2) dmq.coddual.dqmsr.fd_def lra)
 
-lemma cd_dia_demod_subid_var_fres: 
-  assumes "p \<le> 1" 
+lemma cd_dia_demod_subid_var_fres:
+  assumes "p \<le> 1"
   and "q \<le> 1"
 shows "(cd_dia x p \<le> q) = (p \<le> \<top> \<cdot> q \<leftarrow> x)"
   by (simp add: assms cd_dia_demod_subid_var local.fres_galois)
 
-lemma do_box_iso: 
+lemma do_box_iso:
   assumes "p \<le> 1"
-  and "q \<le> 1" 
-  and "p \<le> q" 
+  and "q \<le> 1"
+  and "p \<le> q"
 shows "do_box x p \<le> do_box x q"
   by (meson assms do_box_subid do_dia_do_box_galois local.order.refl local.order.trans)
 
 lemma cd_box_iso:
   assumes "p \<le> 1"
-  and "q \<le> 1" 
-  and "p \<le> q" 
+  and "q \<le> 1"
+  and "p \<le> q"
 shows "cd_box x p \<le> cd_box x q"
   by (metis assms do_box_cd_box_conv do_box_iso)
 
-lemma do_box_demod_subid: 
-  assumes "p \<le> 1" 
+lemma do_box_demod_subid:
+  assumes "p \<le> 1"
   and "q \<le> 1"
   shows "(p \<le> do_box x q) = (x \<cdot> p \<le> q \<cdot> x)"
   using assms do_dia_do_box_galois local.do_dia_demod_subid by force
 
-lemma do_box_demod_subid_bres: 
-  assumes "p \<le> 1" 
+lemma do_box_demod_subid_bres:
+  assumes "p \<le> 1"
   and "q \<le> 1"
   shows "(p \<le> do_box x q) = (p \<le> x \<rightarrow> q \<cdot> x)"
   by (simp add: assms do_box_demod_subid local.bres_galois)
 
-lemma do_box_demod_subid_var: 
-  assumes "p \<le> 1" 
+lemma do_box_demod_subid_var:
+  assumes "p \<le> 1"
   and "q \<le> 1"
   shows "(p \<le> do_box x q) = (x \<cdot> p \<le> q \<cdot> \<top>)"
   using assms do_dia_demod_subid_var do_dia_do_box_galois by auto
 
-lemma do_box_demod_subid_var_bres: 
-  assumes "p \<le> 1" 
+lemma do_box_demod_subid_var_bres:
+  assumes "p \<le> 1"
   and "q \<le> 1"
   shows "(p \<le> do_box x q) = (p \<le> x \<rightarrow> q \<cdot> \<top>)"
   by (simp add: assms do_box_demod_subid_var local.bres_galois)
 
-lemma do_box_demod_subid_var_bres_do: 
-  assumes "p \<le> 1" 
+lemma do_box_demod_subid_var_bres_do:
+  assumes "p \<le> 1"
   and "q \<le> 1"
   shows "(p \<le> do_box x q) = (p \<le> do (x \<rightarrow> q \<cdot> \<top>))"
   by (simp add: assms do_box_demod_subid_var_bres do_top)
 
-lemma cd_box_demod_subid: 
-  assumes "p \<le> 1" 
+lemma cd_box_demod_subid:
+  assumes "p \<le> 1"
   and "q \<le> 1"
   shows "(p \<le> cd_box x q) = (p \<cdot> x \<le> x \<cdot> q)"
   using assms local.cd_dia_cd_box_galois local.cd_dia_demod_subid by force
 
-lemma cd_box_demod_subid_fres: 
-  assumes "p \<le> 1" 
+lemma cd_box_demod_subid_fres:
+  assumes "p \<le> 1"
   and "q \<le> 1"
   shows "(p \<le> cd_box x q) = (p \<le> x \<cdot> q \<leftarrow> x)"
   by (simp add: assms cd_box_demod_subid local.fres_galois)
 
-lemma cd_box_demod_subid_var: 
-  assumes "p \<le> 1" 
+lemma cd_box_demod_subid_var:
+  assumes "p \<le> 1"
   and "q \<le> 1"
   shows "(p \<le> cd_box x q) = (p \<cdot> x \<le> \<top> \<cdot> q)"
   using assms cd_dia_cd_box_galois cd_dia_demod_subid_var by force
 
-lemma cd_box_demod_subid_var_fres: 
-  assumes "p \<le> 1" 
+lemma cd_box_demod_subid_var_fres:
+  assumes "p \<le> 1"
   and "q \<le> 1"
   shows "(p \<le> cd_box x q) = (p \<le> \<top> \<cdot> q \<leftarrow> x)"
   by (simp add: assms cd_box_demod_subid_var local.fres_galois)
 
-text \<open>We substitute demodalisation inequalities for diamonds in the definitions of boxes.\<close> 
+text \<open>We substitute demodalisation inequalities for diamonds in the definitions of boxes.\<close>
 
 lemma do_box_var2: "p \<le> 1 \<Longrightarrow> do_box x p = \<Squnion>{q. x \<cdot> q \<le> p \<cdot> x \<and> q \<le> 1}"
   unfolding do_box_var by (meson do_dia_demod_subid)
 
 lemma do_box_bres1: "p \<le> 1 \<Longrightarrow> do_box x p = \<Squnion>{q. q \<le> x \<rightarrow> p \<cdot> x \<and> q \<le> 1}"
   unfolding do_box_var by (meson do_dia_demod_subid_fres)
 
 lemma do_box_bres2: "p \<le> 1 \<Longrightarrow> do_box x p = \<Squnion>{q. q \<le> x \<rightarrow> p \<cdot> \<top> \<and> q \<le> 1}"
-  unfolding do_box_var by (simp add: dmq.dqmsr.fd_def lla local.bres_galois) 
+  unfolding do_box_var by (simp add: dmq.dqmsr.fd_def lla local.bres_galois)
 
 lemma do_box_var3: "p \<le> 1 \<Longrightarrow> do_box x p = \<Squnion>{q. x \<cdot> q \<le> p \<cdot> \<top> \<and> q \<le> 1}"
   unfolding do_box_var using dmq.dqmsr.fd_def lla by force
 
 lemma cd_box_var2: "p \<le> 1 \<Longrightarrow> cd_box x p = \<Squnion>{q. q \<cdot> x \<le> x \<cdot> p \<and> q \<le> 1}"
   unfolding cd_box_var by (metis cd_dia_demod_subid)
 
 lemma cd_box_var3: "p \<le> 1 \<Longrightarrow> cd_box x p = \<Squnion>{q. q \<cdot> x \<le> \<top> \<cdot> p \<and> q \<le> 1}"
   unfolding cd_box_var by (simp add: dmq.coddual.dqmsr.fd_def lra)
 
 text \<open>Using these results we get a simple characterisation of boxes via domain and codomain.
 Similar laws can be found implicitly in Doornbos, Backhouse and van der Woude's paper on a calculational
 approach to mathematical induction, which speaks about wlp operators instead  modal operators.\<close>
 
 lemma bres_do_box: "p \<le> 1 \<Longrightarrow> do_box x p = do (x \<rightarrow> p \<cdot> \<top>)"
   by (meson do_box_demod_subid_var_bres_do do_box_subid local.cd_fix_subid local.cddo_compat local.dual_order.antisym local.eq_refl)
 
 lemma bres_do_box_var: "p \<le> 1 \<Longrightarrow> do_box x p = 1 \<sqinter> (x \<rightarrow> p \<cdot> \<top>)"
   using bres_do_box do_bres_prop by force
 
 lemma bres_do_box_top: "p \<le> 1 \<Longrightarrow> (do_box x p) \<cdot> \<top> = x \<rightarrow> p \<cdot> \<top>"
   using bres_do_box do_top2 by auto
 
 lemma fres_cd_box: "p \<le> 1 \<Longrightarrow> cd_box x p = cd (\<top> \<cdot> p \<leftarrow> x)"
 proof-
   assume h0: "p \<le> 1"
-  {fix q 
+  {fix q
   assume h1: "q \<le> 1"
   have "(q \<le> cd_box x p) = (q \<cdot> x \<le> \<top> \<cdot> p)"
     by (simp add: cd_box_demod_subid_var h0 h1)
   also have "\<dots> = (q \<le> \<top> \<cdot> p \<leftarrow> x)"
     by (simp add: local.fres_galois)
   also have "\<dots> = (q \<le> 1 \<sqinter> (\<top> \<cdot> p \<leftarrow> x))"
     by (simp add: h1)
   also have "\<dots> = (q \<le> cd (\<top> \<cdot> p \<leftarrow> x))"
     by (simp add: cd_fres_prop h0)
   finally have "(q \<le> cd_box x p) = (q \<le> cd (\<top> \<cdot> p \<leftarrow> x))".}
   hence "\<forall>y. y \<le> cd_box x p \<longleftrightarrow> y \<le> cd (\<top> \<cdot> p \<leftarrow> x)"
     by (meson cd_box_subid dmq.coddual.dqmsr.dpd3 h0 local.dual_order.trans)
   thus ?thesis
     using local.dual_order.antisym by blast
 qed
 
 lemma fres_cd_box_var: "p \<le> 1 \<Longrightarrow> cd_box x p = 1 \<sqinter> (\<top> \<cdot> p \<leftarrow> x)"
   by (simp add: cd_fres_prop fres_cd_box)
 
 lemma fres_cd_box_top: "p \<le> 1 \<Longrightarrow> \<top> \<cdot> cd_box x p = \<top> \<cdot> p \<leftarrow> x"
   using cd_top2 fres_cd_box by auto
 
 
 text \<open>Next we show that the box operators act on the complete Heyting algebra of subidentities.\<close>
 
 lemma cd_box_act:
   assumes "p \<le> 1"
   shows "cd_box (x \<cdot> y) p = cd_box x (cd_box y p)"
 proof-
   {fix q
     assume a: "q \<le> 1"
     hence "(q \<le> cd_box (x \<cdot> y) p) = (cd_dia (x \<cdot> y) q \<le> p)"
       by (simp add: assms cd_dia_cd_box_galois)
     also have "\<dots> = (cd_dia y (cd_dia x q) \<le> p)"
       by (simp add: local.dmq.coddual.dqmsr.fdia_mult)
     also have "\<dots> = (cd_dia x q \<le> cd_box y p)"
       using assms cd_dia_cd_box_galois cd_top dmq.coddual.dqmsr.fd_def by force
     also have "\<dots> = (q \<le> cd_box x (cd_box y p))"
       by (simp add: a assms cd_dia_cd_box_galois local.cd_box_subid)
     finally have "(q \<le> cd_box (x \<cdot> y) p) = (q \<le> cd_box x (cd_box y p))".}
   thus ?thesis
     by (meson assms local.cd_box_subid local.dual_order.eq_iff)
 qed
 
 lemma do_box_act:
   assumes "p \<le> 1"
   shows "do_box (x \<cdot> y) p = do_box y (do_box x p)"
   by (smt (verit) assms cd_box_act local.cd_box_do_box_conv local.do_box_subid local.inv_contrav)
 
-text \<open>Next we show that the box operators are Sup reversing in the first and Inf preserving 
+text \<open>Next we show that the box operators are Sup reversing in the first and Inf preserving
 in the second argument.\<close>
 
 lemma do_box_sup_inf: "p \<le> 1 \<Longrightarrow> do_box (x \<squnion> y) p = do_box x p \<cdot> do_box y p"
 proof-
-  assume h1: "p \<le> 1" 
+  assume h1: "p \<le> 1"
   {fix q
   assume h2: "q \<le> 1"
   hence "(q \<le> do_box (x \<squnion> y) p) = (do_dia (x \<squnion> y) q \<le> p)"
     by (simp add: do_dia_do_box_galois h1)
   also have "\<dots> = (do_dia x q \<le> p \<and> do_dia y q \<le> p)"
     by (simp add: dmq.dqmsr.fdia_add2)
   also have "\<dots> = (q \<le> do_box x p \<and> q \<le> do_box y p)"
     by (simp add: do_dia_do_box_galois h1 h2)
   also have "\<dots> = (q \<le> do_box x p \<cdot> do_box y p)"
     by (simp add: do_box_subid subid_mult_meet)
   finally have "(q \<le> do_box (x \<squnion> y) p) = (q \<le> do_box x p \<cdot> do_box y p)".}
   hence "\<forall>z. z \<le> do_box (x \<squnion> y) p \<longleftrightarrow> z \<le> do_box x p \<cdot> do_box y p"
     by (metis do_box_subid local.dual_order.trans local.inf.boundedE subid_mult_meet)
   thus ?thesis
     using local.dual_order.antisym by blast
 qed
 
 lemma do_box_sup_inf_var: "p \<le> 1 \<Longrightarrow> do_box (x \<squnion> y) p = do_box x p \<sqinter> do_box y p"
   by (simp add: do_box_subid do_box_sup_inf subid_mult_meet)
 
-lemma do_box_Sup_Inf: 
+lemma do_box_Sup_Inf:
   assumes "X \<noteq> {}"
   and "p \<le> 1"
   shows "do_box (\<Squnion>X) p = (\<Sqinter>x \<in> X. do_box x p)"
 proof-
   {fix q
     assume h: "q \<le> 1"
     hence "(q \<le> do_box (\<Squnion>X) p) = (do_dia (\<Squnion>X) q \<le> p)"
     by (simp add: do_dia_do_box_galois assms(2))
   also have "\<dots> = ((\<Squnion>x \<in> X. do_dia x q) \<le> p)"
     using do_dia_Sup by force
   also have "\<dots> = (\<forall>x \<in> X. do_dia x q \<le> p)"
     by (simp add: local.SUP_le_iff)
   also have "\<dots> = (\<forall>x \<in> X. q \<le> do_box x p)"
     using do_dia_do_box_galois assms(2) h by blast
   also have "\<dots> = (q \<le> (\<Sqinter>x \<in> X. do_box x p))"
     by (simp add: local.le_INF_iff)
   finally have "(q \<le> do_box (\<Squnion>X) p) = (q \<le> (\<Sqinter>x \<in> X. do_box x p))".}
   hence "\<forall>y. y \<le> do_box (\<Squnion>X) p \<longleftrightarrow> y \<le> (\<Sqinter>x \<in> X. do_box x p)"
     by (smt (verit, ccfv_threshold) assms(1) do_box_subid local.INF_le_SUP local.SUP_least local.order_trans)
   thus ?thesis
     using local.dual_order.antisym by blast
 qed
 
-lemma do_box_Sup_Inf2: 
+lemma do_box_Sup_Inf2:
   assumes "P \<noteq> {}"
   and "\<forall>p \<in> P. p \<le> 1"
   shows "do_box x (\<Sqinter>P) = (\<Sqinter>p \<in> P. do_box x p)"
 proof-
   have h0: "(\<Sqinter>p \<in> P. do_box x p) \<le> 1"
   by (meson all_not_in_conv assms(1) do_box_subid local.INF_lower2)
   {fix q
     assume h1: "q \<le> 1"
     hence "(q \<le> do_box x (\<Sqinter>P)) = (do_dia x q \<le> \<Sqinter>P)"
       by (simp add: assms do_dia_do_box_galois local.Inf_less_eq)
     also have "\<dots> = (\<forall>p \<in> P. do_dia x q \<le> p)"
       using local.le_Inf_iff by blast
     also have "\<dots> = (\<forall>p \<in> P. q \<le> do_box x p)"
       using assms(2) do_dia_do_box_galois h1 by auto
     also have "\<dots> = (q \<le> (\<Sqinter>p \<in> P. do_box x p))"
       by (simp add: local.le_INF_iff)
     finally have "(q \<le> do_box x (\<Sqinter>P)) = (q \<le> (\<Sqinter>p \<in> P. do_box x p))".}
   thus ?thesis
     using do_box_subid h0 local.dual_order.antisym by blast
 qed
 
 lemma cd_box_sup_inf: "p \<le> 1 \<Longrightarrow> cd_box (x \<squnion> y) p = cd_box x p \<cdot> cd_box y p"
   by (metis do_box_cd_box_conv do_box_sup_inf local.inv_binsup)
 
 lemma cd_box_sup_inf_var: "p \<le> 1 \<Longrightarrow> cd_box (x \<squnion> y) p = cd_box x p \<sqinter> cd_box y p"
   by (simp add: cd_box_subid cd_box_sup_inf subid_mult_meet)
 
-lemma cd_box_Sup_Inf: 
+lemma cd_box_Sup_Inf:
   assumes "X \<noteq> {}"
   and "p \<le> 1"
 shows "cd_box (\<Squnion>X) p = (\<Sqinter>x \<in> X. cd_box x p)"
 proof-
   have "cd_box (\<Squnion>X) p = do_box ((\<Squnion>X)\<^sup>\<circ>) p"
     using assms(2) do_box_cd_box_conv by presburger
   also have "\<dots> = (\<Sqinter>y \<in> {x\<^sup>\<circ>|x. x \<in> X}. do_box y p)"
     by (simp add: Setcompr_eq_image assms do_box_Sup_Inf)
   also have "\<dots> = (\<Sqinter>x \<in> X. do_box (x\<^sup>\<circ>) p)"
     by (simp add: Setcompr_eq_image image_image)
   also have "\<dots> = (\<Sqinter>x \<in> X. cd_box x p)"
     using assms(2) do_box_cd_box_conv by force
   finally show ?thesis.
 qed
 
-lemma cd_box_Sup_Inf2: 
+lemma cd_box_Sup_Inf2:
   assumes "P \<noteq> {}"
   and "\<forall>p \<in> P. p \<le> 1"
 shows "cd_box x (\<Sqinter>P) = (\<Sqinter>p \<in> P. cd_box x p)"
 proof-
   have "cd_box x (\<Sqinter>P) = do_box (x\<^sup>\<circ>) (\<Sqinter>P)"
     by (simp add: assms do_box_cd_box_conv local.Inf_less_eq)
   also have "\<dots> = (\<Sqinter>p \<in> P. do_box (x\<^sup>\<circ>) p)"
     using assms do_box_Sup_Inf2 by presburger
   also have "\<dots> = (\<Sqinter>p \<in> P. cd_box x p)"
     using assms(2) do_box_cd_box_conv by force
   finally show ?thesis.
 qed
 
-text \<open>Next we define an antidomain operation in the style of modal semirings. A natural condition is 
-that the antidomain of an element is the greatest test that cannot be left-composed with that elements, 
-and hence a greatest left annihilator. The definition of anticodomain is similar. As we are not in a 
-boolean domain algebra, we cannot expect that the antidomain of the antidomain yields the domain or 
+text \<open>Next we define an antidomain operation in the style of modal semirings. A natural condition is
+that the antidomain of an element is the greatest test that cannot be left-composed with that elements,
+and hence a greatest left annihilator. The definition of anticodomain is similar. As we are not in a
+boolean domain algebra, we cannot expect that the antidomain of the antidomain yields the domain or
 that the union of a domain element with the corresponding antidomain element equals one.\<close>
 
 definition "ado x = \<Squnion>{p. p \<cdot> x = \<bottom> \<and> p \<le> 1}"
 
 definition "acd x = \<Squnion>{p. x \<cdot> p = \<bottom> \<and> p \<le> 1}"
 
 lemma ado_acd: "ado (x\<^sup>\<circ>) = acd x"
   unfolding ado_def acd_def
   by (metis convdqka.subid_conv invqka.inv_zero local.inv_contrav local.inv_invol)
 
 lemma acd_ado: "acd (x\<^sup>\<circ>) = ado x"
   unfolding ado_def acd_def
   by (metis acd_def ado_acd ado_def local.inv_invol)
 
 lemma ado_left_zero [simp]: "ado x \<cdot> x = \<bottom>"
   unfolding ado_def
   using dmq.coddual.Sup_distl by auto
 
 lemma acd_right_zero [simp]: "x \<cdot> acd x = \<bottom>"
   unfolding acd_def
   by (simp add: dmq.coddual.h_Sup local.dual_order.antisym)
 
 lemma ado_greatest: "p \<le> 1 \<Longrightarrow> p \<cdot> x = \<bottom> \<Longrightarrow> p \<le> ado x"
   by (simp add: ado_def local.Sup_upper)
 
 lemma acd_greatest: "p \<le> 1 \<Longrightarrow> x \<cdot> p = \<bottom> \<Longrightarrow> p \<le> acd x"
   by (simp add: acd_def local.Sup_upper)
 
 lemma ado_subid: "ado x \<le> 1"
   using ado_def local.Sup_le_iff by force
 
 lemma acd_subid: "acd x \<le> 1"
   by (simp add: acd_def local.Sup_le_iff)
 
 lemma ado_left_zero_iff: "p \<le> 1 \<Longrightarrow> (p \<le> ado x) = (p \<cdot> x = \<bottom>)"
   by (metis ado_greatest ado_left_zero local.bot_unique local.mult_isor)
 
 lemma acd_right_zero_iff: "p \<le> 1 \<Longrightarrow> (p \<le> acd x) = (x \<cdot> p = \<bottom>)"
   by (metis acd_greatest acd_right_zero local.bot_unique local.mult_isol)
 
 text \<open>This gives an eqational characterisation of antidomain and anticodomain.\<close>
 
 lemma ado_cd_bot: "ado x = cd (\<bottom> \<leftarrow> x)"
 proof-
   {fix p
   assume  h: "p \<le> 1"
   hence "(p \<le> ado x) = (p \<cdot> x = \<bottom>)"
-    by (simp add: ado_left_zero_iff) 
+    by (simp add: ado_left_zero_iff)
   also have "\<dots> = (p \<le> \<bottom> \<leftarrow> x)"
     using local.bot_unique local.fres_galois by blast
   also have "\<dots> = (p \<le> 1 \<sqinter> (\<bottom> \<leftarrow> x))"
     by (simp add: h)
   also have "\<dots> = (p \<le> cd (\<bottom> \<leftarrow> x))"
     by (metis cd_fres_prop local.bot_least local.mult_botr)
   finally have "(p \<le> ado x) = (p \<le> cd (\<bottom> \<leftarrow> x))".}
   hence "\<forall>y. y \<le> ado x \<longleftrightarrow> y \<le> cd (\<bottom> \<leftarrow> x)"
     using ado_subid local.cd_subid local.dual_order.trans by blast
   thus ?thesis
     using local.dual_order.antisym by blast
 qed
 
 lemma acd_do_bot: "acd x = do (x \<rightarrow> \<bottom>)"
   by (metis ado_acd ado_cd_bot invqka.inv_zero local.bres_fres_conv local.cd_inv local.inv_invol)
 
 lemma ado_cd_bot_id: "ado x = 1 \<sqinter> (\<bottom> \<leftarrow> x)"
   by (metis ado_cd_bot cd_fres_prop local.cd_bot local.cd_subid local.mult_botr)
 
 lemma acd_do_bot_id: "acd x = 1 \<sqinter> (x \<rightarrow> \<bottom>)"
   by (metis acd_do_bot do_bres_prop local.bot_least local.mult_botl)
 
 lemma ado_cd_bot_var: "ado x = cd (\<bottom> \<leftarrow> do x)"
   by (metis ado_cd_bot do_top2 local.fres_bot_top local.fres_curry)
 
 lemma acd_do_bot_var: "acd x = do (cd x \<rightarrow> \<bottom>)"
   by (metis acd_do_bot cd_top2 local.bres_curry local.bres_top_bot)
 
 lemma ado_do_bot: "ado x = do (do x \<rightarrow> \<bottom>)"
   using acd_ado acd_do_bot_var local.cd_inv by auto
 
 lemma "do x = ado (ado x)" (* nitpick[expect=genuine]*)
-  oops 
+  oops
 
 lemma acd_cd_bot: "acd x = cd (\<bottom> \<leftarrow> cd x)"
   by (metis ado_acd ado_cd_bot_var local.cd_inv local.inv_invol)
 
 lemma ado_do_bot_var: "ado x = 1 \<sqinter> (do x \<rightarrow> \<bottom>)"
   by (metis ado_do_bot do_bres_prop local.bot_unique local.bres_bot_bot local.bres_canc1 local.do_bot local.do_subid)
 
  lemma acd_cd_bot_var: "acd x = 1 \<sqinter> (\<bottom> \<leftarrow> cd x)"
    by (metis acd_cd_bot acd_right_zero cd_top local.fres_top_top2)
 
 
 text \<open>Domain and codomain are compatible with the boxes.\<close>
 
 lemma cd_box_ado: "cd_box x \<bottom> = ado x"
   by (simp add: ado_cd_bot fres_cd_box)
 
 lemma do_box_acd: "do_box x \<bottom> = acd x"
   by (simp add: acd_do_bot bres_do_box)
 
 lemma ado_subid_prop: "p \<le> 1 \<Longrightarrow> ado p = 1 \<sqinter> (p \<rightarrow> \<bottom>)"
   by (metis ado_do_bot_var do_fix_subid)
 
 lemma ado_do: "p \<le> 1 \<Longrightarrow> ado p = do (p \<rightarrow> \<bottom>)"
   using ado_do_bot do_fix_subid by force
 
 lemma ado_do_compl: "ado x \<cdot> do x = \<bottom>"
   using dmq.dqmsr.dom_weakly_local by force
 
 lemma "ado x \<squnion> do x = \<top>" (* nitpick[expect = genuine]*)
   oops
 
 lemma "\<forall>x p. \<exists>f. 1 \<sqinter> (\<top> \<cdot> p \<leftarrow> x) = 1 \<sqinter> (\<bottom> \<leftarrow> (x \<rightarrow> p \<cdot> \<top>))" (* nitpick[expect=genuine]*)
   oops
 
 lemma "cd_box x p = ado (x \<cdot> ado p)" (* nitpick[expect=genuine]*)
   oops
 
 lemma ad_do_bot [simp]: "(1 \<sqinter> (do x \<rightarrow> \<bottom>)) \<cdot> do x = \<bottom>"
   using ado_do_bot_var ado_left_zero dmq.dqmsr.dom_weakly_local by presburger
- 
+
 lemma do_heyting_galois: "(do x \<cdot> do y \<le> do z) = (do x \<le> 1 \<sqinter> (do y \<rightarrow> do z))"
   by (metis dmq.dqmsr.dsg4 dmq.mqdual.cod_subid local.bres_galois local.le_inf_iff)
 
 lemma do_heyting_galois_var: "(do x \<cdot> do y \<le> do z) = (do x \<le> cd_box (do y) (do z))"
   by (metis cd_dia_cd_box_galois cd_fix_subid dmq.coddual.dqmsr.fd_def dmq.dqmsr.dom_mult_closed local.do_subid)
 
 text \<open>Antidomain is therefore Heyting negation.\<close>
 
 lemma ado_heyting_negation: "ado (do x) = cd_box (do x) \<bottom>"
   by (simp add: cd_box_ado)
 
 lemma ad_ax1 [simp]: "(1 \<sqinter> (do x \<rightarrow> \<bottom>)) \<cdot> x = \<bottom>"
   by (simp add: local.dmq.dqmsr.dom_weakly_local)
 
 lemma "1 \<sqinter> (do (1 \<sqinter> (do x \<rightarrow> \<bottom>)) \<rightarrow> \<bottom>) = do x" (* nitpick[expect=genuine]*)
   oops
 
 lemma "p \<le> 1 \<Longrightarrow> do_dia x p = 1 \<sqinter> (cd_box x (1 \<sqinter> (p \<rightarrow> \<bottom>)) \<rightarrow> \<bottom>)" (* nitpick[expect=genuine]*)
   oops
 
 lemma  "p \<le> 1 \<Longrightarrow> cd_box x p = 1 \<sqinter> (do_dia x (1 \<sqinter> (p \<rightarrow> \<bottom>)) \<rightarrow> \<bottom>)" (* nitpick[expect=genuine]*)
   oops
 
 lemma "p \<le> 1 \<Longrightarrow> cd_dia x p = 1 \<sqinter> (do_box x (1 \<sqinter> (p \<rightarrow> \<bottom>)) \<rightarrow> \<bottom>)" (* nitpick[expect=genuine]*)
   oops
 
 lemma "p \<le> 1 \<Longrightarrow> do_box x p = 1 \<sqinter> (cd_dia x (1 \<sqinter> (p \<rightarrow> \<bottom>)) \<rightarrow> \<bottom>)" (* nitpick[expect=genuine]*)
   oops
 
 end
 
 subsection \<open>Boolean Dedekind quantales\<close>
 
 class distributive_dedekind_quantale = distrib_unital_quantale + dedekind_quantale
 
 class boolean_dedekind_quantale = bool_unital_quantale + distributive_dedekind_quantale
 
 begin
 
 lemma ad_do_bot [simp]: "(1 - do x) \<cdot> do x = \<bottom>"
   by (simp add: local.diff_eq local.inf_shunt local.subid_mult_meet)
 
 lemma ad_ax1 [simp]: "(1 - do x) \<cdot> x = \<bottom>"
   by (simp add: local.dmq.dqmsr.dom_weakly_local)
 
 lemma ad_do [simp]: "1 - do (1 - do x) = do x"
 proof-
   have "1 - do (1 - do x) = 1 - (1 - do x)"
     by (metis local.diff_eq local.do_fix_subid local.inf.cobounded1)
   also have "\<dots> = 1 \<sqinter> -(1 \<sqinter> - do x)"
     by (simp add: local.diff_eq)
   also have "\<dots> = do x"
     by (simp add: local.chaq.wswq.distrib_left local.do_top)
   finally show ?thesis.
 qed
 
 lemma ad_ax2: "1 - do (x \<cdot> y) \<squnion> (1 - do (x \<cdot> (1 - do (1 - do y)))) = 1 - do (x \<cdot> (1 - do (1 - do y)))"
   by simp
 
 lemma ad_ax3 [simp]: "do x \<squnion> (1 - do x) = 1"
 proof-
   have "do x \<squnion> (1 - do x) = do x \<squnion> (1 \<sqinter> -do x)"
     using local.diff_eq by force
   also have "\<dots> = 1 \<sqinter> (do x \<squnion> -do x)"
     by (simp add: local.chaq.wswq.distrib_left local.do_top)
   also have "\<dots> = 1"
     by simp
   finally show ?thesis.
 qed
 
-sublocale bdad: antidomain_semiring "\<lambda>x. 1 - do x" "(\<squnion>)" "(\<cdot>)" 1 \<bottom> _ _ 
+sublocale bdad: antidomain_semiring "\<lambda>x. 1 - do x" "(\<squnion>)" "(\<cdot>)" 1 \<bottom> _ _
   by unfold_locales simp_all
 
 sublocale bdadka: antidomain_kleene_algebra "\<lambda>x. 1 - do x" "(\<squnion>)" "(\<cdot>)" 1 \<bottom> _ _ qstar..
 
 sublocale bdar: antirange_semiring "(\<squnion>)" "(\<cdot>)" 1 \<bottom> "\<lambda>x. 1 - cd x" _ _
   apply unfold_locales
     apply (metis ad_ax1 ad_do dmq.mqs.local_var local.docd_compat)
    apply (metis ad_do local.cddo_compat local.dmq.coddual.dqmsr.dsr2 local.docd_compat local.sup.idem)
   by (metis bdad.a_subid' bdad.as3 local.convdqka.subid_conv local.do_inv)
 
 sublocale bdaka: antirange_kleene_algebra "(\<squnion>)" "(\<cdot>)" 1 \<bottom> _ _ qstar "\<lambda>x. 1 - cd x"..
 
 sublocale bmod: modal_semiring_simp "\<lambda>x. 1 - do x" "(\<squnion>)" "(\<cdot>)" 1 \<bottom> _ _ "\<lambda>x. 1 - cd x"..
 
 sublocale bmod: modal_kleene_algebra_simp "(\<squnion>)" "(\<cdot>)" 1 \<bottom> _ _ qstar "\<lambda>x. 1 - do x" "\<lambda>x. 1 - cd x"..
 
 lemma inv_neg: "(-x)\<^sup>\<circ> = -(x\<^sup>\<circ>)"
   by (metis local.diff_eq local.diff_shunt_var local.dual_order.eq_iff local.inf.commute local.inv_conjugate local.inv_galois)
 
 lemma residuation: "x\<^sup>\<circ> \<cdot> -(x \<cdot> y) \<le> -y"
   by (metis local.inf.commute local.inf_compl_bot local.inf_shunt local.schroeder_1)
 
 lemma bres_prop: "x \<rightarrow> y = -(x\<^sup>\<circ> \<cdot> -y)"
   by (metis local.ba_dual.dual_iff local.bres_canc1 local.bres_galois_imp local.compl_le_swap1 local.dmq.coddual.h_w1 local.dual_order.antisym local.inv_invol residuation)
 
 lemma fres_prop: "x \<leftarrow> y = -(-x \<cdot> y\<^sup>\<circ>)"
   using bres_prop inv_neg local.fres_bres_conv by auto
 
 lemma do_dia_fdia: "do_dia x p = bdad.fdia x p"
   by (simp add: local.bdad.fdia_def local.dmq.dqmsr.fd_def)
 
 lemma cd_dia_bdia: "cd_dia x p = bdar.bdia x p"
   by (metis ad_do bdar.ardual.a_subid' bdar.bdia_def local.cd_fix_subid local.dmq.coddual.dqmsr.fd_def local.docd_compat)
 
 lemma do_dia_fbox_de_morgan: "p \<le> 1 \<Longrightarrow> do_dia x p = 1 - bdad.fbox x (1 - p)"
   by (smt (verit, ccfv_SIG) ad_do bdad.a_closure bdad.am_d_def bdad.fbox_def local.dmq.dqmsr.fd_def local.do_fix_subid)
 
 lemma fbox_do_dia_de_morgan: "p \<le> 1 \<Longrightarrow> bdad.fbox x p = 1 - do_dia x (1 - p)"
   using bdad.fbox_def local.dmq.dqmsr.fd_def local.do_fix_subid by force
 
 lemma cd_dia_bbox_de_morgan: "p \<le> 1 \<Longrightarrow> cd_dia x p = 1 - bdar.bbox x (1 - p)"
   by (smt (verit, best) ad_do bdar.bbox_def bdar.bdia_def cd_dia_bdia local.cd_fix_subid local.do_subid local.docd_compat)
 
 lemma bbox_cd_dia_de_morgan: "p \<le> 1 \<Longrightarrow> bdar.bbox x p = 1 - cd_dia x (1 - p)"
   using bdar.bbox_def local.cd_fix_subid local.dmq.coddual.dqmsr.fd_def by force
 
 lemma do_box_bbox: "p \<le> 1 \<Longrightarrow> do_box x p = bdar.bbox x p"
 proof-
   assume a: "p \<le> 1"
   {fix q
   assume b: "q \<le> 1"
   hence "(q \<le> do_box x p) = (x \<cdot> q \<le> p \<cdot> x)"
     by (simp add: a local.do_box_demod_subid)
   also have "\<dots> = (x \<cdot> cd q \<le> cd p \<cdot> x)"
     by (metis a b local.cd_fix_subid)
   also have "\<dots> = (cd q \<le> bdar.bbox x p)"
    by (metis bdar.bbox_def bdar.bdia_def cd_dia_bdia local.bdar.ardual.a_closure' local.bdar.ardual.ans_d_def local.bdar.ardual.dnsz.dsg1 local.bdar.ardual.fbox_demodalisation3 local.bdar.ardual.fbox_one local.dmq.coddual.dqmsr.fd_def local.nsrnqo.mult_oner)
   also have "\<dots> = (q \<le> bdar.bbox x p)"
     using b local.cd_fix_subid by force
   finally have "(q \<le> do_box x p) = (q \<le> bdar.bbox x p)".}
   thus ?thesis
     by (metis bdar.bbox_def local.bdar.ardual.a_subid' local.do_box_subid local.dual_order.antisym local.eq_refl)
 qed
 
 lemma cd_box_fbox: "p \<le> 1 \<Longrightarrow> cd_box x p = bdad.fbox x p"
   by (smt (verit, ccfv_SIG) bdar.bbox_def do_box_bbox local.bdad.fbox_def local.cd_dia_do_dia_conv local.cd_inv local.cd_fix_subid local.cd_top local.diff_eq local.dmq.bb_def local.dmq.coddual.dqmsr.fd_def local.dmq.coddual.mult_assoc local.dmq.dqmsr.fd_def local.dmq.fb_def local.do_box_cd_box_conv local.do_fix_subid local.do_top local.inf.cobounded1)
 
 lemma do_dia_cd_box_de_morgan: "p \<le> 1 \<Longrightarrow> do_dia x p = 1 - cd_box x (1 - p)"
   by (simp add: cd_box_fbox local.diff_eq local.do_dia_fbox_de_morgan)
 
 lemma cd_box_do_dia_de_morgan: "p \<le> 1 \<Longrightarrow> cd_box x p = 1 - do_dia x (1 - p)"
   by (simp add: cd_box_fbox local.fbox_do_dia_de_morgan)
 
 lemma cd_dia_do_box_de_morgan: "p \<le> 1 \<Longrightarrow> cd_dia x p = 1 - do_box x (1 - p)"
   by (simp add: do_box_bbox local.cd_dia_bbox_de_morgan local.diff_eq)
 
 lemma do_box_cd_dia_de_morgan: "p \<le> 1 \<Longrightarrow> do_box x p = 1 - cd_dia x (1 - p)"
   by (simp add: do_box_bbox local.bbox_cd_dia_de_morgan)
 
 end
 
 class dc_involutive_modal_quantale = dc_modal_quantale + involutive_quantale
 
 begin
 
 sublocale invmqmka: involutive_dr_modal_kleene_algebra "(\<squnion>)" "(\<cdot>)" 1 \<bottom> "(\<le>)" "(<)" qstar invol dom cod..
 
 lemma do_approx_dom: "do x \<le> dom x"
 proof -
   have "do x = dom (do x) \<cdot> do x"
     by simp
   also have "\<dots> \<le> dom (1 \<sqinter> (x \<cdot> x\<^sup>\<circ>))"
     by (simp add: local.do_def local.dqmsr.domain_subid)
   also have "\<dots> \<le> dom 1 \<sqinter> dom (x \<cdot>  x\<^sup>\<circ>)"
     using local.dom_meet_sub by presburger
   also have "\<dots> \<le> dom (x \<cdot> dom (x\<^sup>\<circ>))"
     by simp
   also have "\<dots> \<le> dom x"
     by (simp add: local.dqmsr.domain_1'')
   finally show ?thesis.
 qed
 
 end
 
 class dc_modal_quantale_converse = dc_involutive_modal_quantale + quantale_converse
 
 sublocale dc_modal_quantale_converse \<subseteq> invmqmka: dr_modal_kleene_algebra_converse  "(\<squnion>)" "(\<cdot>)" 1 \<bottom> "(\<le>)" "(<)" qstar invol dom cod..
 
-class dc_modal_quantale_strong_converse = dc_involutive_modal_quantale +  
+class dc_modal_quantale_strong_converse = dc_involutive_modal_quantale +
   assumes weak_dom_def: "dom x \<le> x \<cdot> x\<^sup>\<circ>"
   and weak_cod_def: "cod x \<le> x\<^sup>\<circ> \<cdot> x"
 
 begin
 
 sublocale invmqmka: dr_modal_kleene_algebra_strong_converse  "(\<squnion>)" "(\<cdot>)" 1 \<bottom> "(\<le>)" "(<)" qstar invol dom cod
   by (unfold_locales, simp_all add: local.weak_dom_def local.weak_cod_def)
 
 lemma dom_def: "dom x = 1 \<sqinter> (x \<cdot> x\<^sup>\<circ>)"
   using local.do_approx_dom local.do_def local.dual_order.eq_iff local.weak_dom_def by force
 
 lemma cod_def: "cod x = 1 \<sqinter> (x\<^sup>\<circ> \<cdot> x)"
   using local.dom_def local.invmqmka.d_conv_cod by auto
 
 lemma do_dom: "do x = dom x"
   by (simp add: local.do_def local.dom_def)
 
 lemma cd_cod: "cd x = cod x"
   by (simp add: local.cd_def local.cod_def)
 
 end
 
-class dc_modal_dedekind_quantale = dc_involutive_modal_quantale + dedekind_quantale 
+class dc_modal_dedekind_quantale = dc_involutive_modal_quantale + dedekind_quantale
 
 class cd_distributive_modal_dedekind_quantale = dc_modal_dedekind_quantale + distrib_unital_quantale
 
 class dc_boolean_modal_dedekind_quantale = dc_modal_dedekind_quantale + bool_unital_quantale
 
 begin
 
 lemma subid_idem: "p \<le> 1 \<Longrightarrow> p \<cdot> p = p"
   by (simp add: local.subid_mult_meet)
 
 lemma subid_comm: "p \<le> 1 \<Longrightarrow> q \<le> 1 \<Longrightarrow> p \<cdot> q = q \<cdot> p"
   using local.inf.commute local.subid_mult_meet by force
 
 lemma subid_meet_comp: "p \<le> 1 \<Longrightarrow> q \<le> 1 \<Longrightarrow> p \<sqinter> q = p \<cdot> q"
   by (simp add: local.subid_mult_meet)
 
 lemma subid_dom: "p \<le> 1 \<Longrightarrow> dom p = p"
 proof-
   assume h: "p \<le> 1"
   have a: "p \<squnion> (1 \<sqinter> -p) = 1"
     by (metis h local.inf_sup_absorb local.sup.commute local.sup.orderE local.sup_compl_top local.sup_inf_distrib1)
   have b: "(1 \<sqinter> -p) \<sqinter> p = \<bottom>"
     by (simp add: local.inf.commute)
   hence "dom p = (p \<squnion> (1 \<sqinter> -p)) \<cdot> dom p"
     by (simp add: a)
   also have "\<dots> = p \<cdot> dom p \<squnion> dom ((1 \<sqinter> -p) \<cdot> dom p) \<cdot> (1 \<sqinter> -p) \<cdot> dom p"
     using local.dqmsr.dsg1 local.wswq.distrib_right mult_assoc by presburger
   also have "\<dots> \<le> p \<squnion> dom ((1 \<sqinter> -p) \<cdot> dom p)"
     by (metis b h local.dom_subid local.dom_zero local.inf.cobounded1 local.mqdual.cod_local local.mult_botr local.sup.mono subid_comm subid_meet_comp)
   also have "\<dots> = p \<squnion> dom ((1 \<sqinter> -p) \<cdot> p)"
     by simp
   also have "\<dots> = p \<squnion> dom \<bottom>"
     using b h subid_meet_comp by fastforce
   also have "\<dots> = p"
     by simp
   finally have "dom p \<le> p".
   thus ?thesis
     using h local.dqmsr.domain_subid local.dual_order.antisym by presburger
 qed
 
 lemma do_prop: "(do x \<le> do y) = (x \<le> do y \<cdot> \<top>)"
   by (simp add: local.lla)
 
 lemma do_lla: "(do x \<le> do y) = (x \<le> do y \<cdot> x)"
   by (simp add: local.lla_var)
 
 lemma lla_subid: "p \<le> 1 \<Longrightarrow> ((dom x \<le> p) = (x \<le> p \<cdot> x))"
   by (metis local.dqmsr.dom_llp subid_dom)
 
 lemma dom_do: "dom x = do x"
 proof-
   have "x \<le> do x \<cdot> x"
     by simp
   hence "dom x \<le> do x"
     using lla_subid local.do_subid local.dodo by presburger
   thus ?thesis
     by (simp add: local.antisym_conv local.do_approx_dom)
 qed
 
 end
 
 end
 
diff --git a/thys/Quantales_Converse/ROOT b/thys/Quantales_Converse/ROOT
--- a/thys/Quantales_Converse/ROOT
+++ b/thys/Quantales_Converse/ROOT
@@ -1,20 +1,20 @@
 chapter AFP
 
 session "Quantales_Converse" (AFP) = HOL +
-  options [timeout = 600]
+  options [timeout = 1200]
 
   sessions
    Kleene_Algebra
-   KAD 
-   Quantales 
-   
+   KAD
+   Quantales
+
   theories
     Modal_Kleene_Algebra_Var
     Kleene_Algebra_Converse
     Modal_Kleene_Algebra_Converse
     Modal_Quantale
     Quantale_Converse
-    
+
   document_files
    "root.tex"
    "root.bib"