Theory Kneser_Cauchy_Davenport_main_proofs

section‹Kneser's Theorem and the Cauchy–Davenport Theorem: main proofs›

(*
  Session: Kneser_Cauchy_Davenport
  Title:   Kneser_Cauchy_Davenport_main_proofs.thy
  Authors: Mantas Bakšys and Angeliki Koutsoukou-Argyraki, University of Cambridge.
  Date: September 2022
*)

theory Kneser_Cauchy_Davenport_main_proofs
  imports 
  Kneser_Cauchy_Davenport_preliminaries

begin

context additive_abelian_group

begin

subsection‹Proof of Kneser's Theorem›

text‹The proof we formalise follows the paper \cite{DeVos_Kneser}. This version of Kneser's Theorem 
corresponds to Theorem 3.2 in \cite{Ruzsa_book}, or to Theorem 4.3 in \cite{Nathanson_book}.  ›

theorem Kneser:
  assumes "A  G" and "B  G" and "finite A" and "finite B" and hAne: "A  {}" and hBne: "B  {}"
  shows "card (sumset A B)   card (sumset A (stabilizer (sumset A B))) + 
    card (sumset B (stabilizer (sumset A B))) - card (stabilizer (sumset A B))"
proof-
  have " n A B. additive_abelian_group G (⊕) 𝟬  A  G  B  G  
    finite A  finite B  A  {}  B  {}   card (sumset A B) + card A = n 
    card (sumset A B)   card (sumset A (stabilizer (sumset A B))) + 
    card (sumset B (stabilizer (sumset A B))) - card ((stabilizer (sumset A B)))"
  proof-
    fix n
    show " A B. additive_abelian_group G (⊕) 𝟬  A  G  B  G  
    finite A  finite B  A  {}  B  {}   card (sumset A B) + card A = n 
    card (sumset A B)   card (sumset A (stabilizer (sumset A B))) + 
    card (sumset B (stabilizer (sumset A B))) - card ((stabilizer (sumset A B)))"
    proof(induction n arbitrary : G "(⊕)" 𝟬 rule: nat_less_induct)
      fix n 
      fix A B G :: "'a set"
      fix add (infixl "[⊕]" 65)
      fix zero ("[𝟬]")
      assume hind: "m<n. x xa xb :: 'a set.  xc xd. 
        additive_abelian_group xb xc xd  x  xb 
        xa  xb  finite x  finite xa  x  {}  xa  {} 
        card (additive_abelian_group.sumset xb xc x xa) + card x = m 
        card (additive_abelian_group.sumset xb xc x (additive_abelian_group.stabilizer xb xc
        (additive_abelian_group.sumset xb xc x xa))) + card (additive_abelian_group.sumset xb xc xa
        (additive_abelian_group.stabilizer xb xc (additive_abelian_group.sumset xb xc x xa))) -
        card (additive_abelian_group.stabilizer xb xc (additive_abelian_group.sumset xb xc x xa))
         card (additive_abelian_group.sumset xb xc x xa)" and 
        hGroupG: "additive_abelian_group G ([⊕]) [𝟬]" and hAG: "A  G" and hBG: "B  G" and 
        hA: "finite A" and hB: "finite B" and hAne: "A  {}" and hBne: "B  {}" and
        hcardsum: "card (additive_abelian_group.sumset G ([⊕]) A B) + card A = n"
      interpret G: additive_abelian_group G "([⊕])" "[𝟬]" using hGroupG by simp
      have hindG: "m<n. C D. C  G 
        D  G  finite C  finite D  C  {}  D  {} 
        card (G.sumset C D) + card C = m 
        card (G.sumset C (G.stabilizer
        (G.sumset C D))) + card (G.sumset D
        (G.stabilizer (G.sumset C D))) -
        card (G.stabilizer (G.sumset C D))
         card (G.sumset C D)" using hind hGroupG by blast
      show "card (G.sumset A (G.stabilizer (G.sumset A B))) + 
        card (G.sumset B (G.stabilizer (G.sumset A B))) - 
        card (G.stabilizer (G.sumset A B))  card (G.sumset A B)"
      proof(cases "G.stabilizer (G.sumset A B) = {[𝟬]}")
        case hstab0: True
        show ?thesis
        proof (cases "card A = 1")
          case True
          then obtain a where "A = {a}" and "a  G"
            by (metis hAG card_1_singletonE insert_subset)
          then show ?thesis using G.card_sumset_singleton_subset_eq 
            G.stabilizer_left_sumset_invariant G.stabilizer_subset_group G.sumset_commute 
            G.sumset_stabilizer_eq_self hBG by (metis diff_add_inverse eq_imp_le)
        next
          case False
          then have "card A  2" using Suc_1 order_antisym_conv
            by (metis Suc_eq_plus1 bot.extremum card_seteq hA hAne le_add2 not_less_eq_eq)
          then obtain a a' where haA: "{a', a}  A" and hanot: "a'  a" and ha1G: "a  G" and 
            ha2G: "a'  G"
            by (smt (verit, ccfv_threshold) card_2_iff hAG insert_subset 
                obtain_subset_with_card_n subset_trans)
          then have "(a' [⊕] (G.inverse a))  G.stabilizer B" using G.stabilizer_sub_sumset_right 
            hstab0 subset_singletonD by (metis G.commutative G.inverse_closed 
            G.invertible G.invertible_right_inverse2 G.right_unit empty_iff insert_iff)
          then obtain b where hb: "b  B" and "(a' [⊕] (G.inverse a)) [⊕] b  B" 
            using G.stabilizer_def G.not_mem_stabilizer_obtain hBG hB hBne ha1G ha2G 
            G.composition_closed G.inverse_closed by (metis (no_types, lifting))
          then have habG: "a' [⊕] b [⊕] G.inverse a  B" 
            using hb hBG ha1G ha2G by (metis G.associative G.commutative G.inverse_closed subset_iff)
          have hbG: "b  G" using hb hBG by auto
          let ?B' = "G.sumset (G.differenceset B {b}) {a}"
          have hB': "finite ?B'" using hB
            by (simp add: G.finite_minusset G.finite_sumset)
          have hB'G: "?B'  G" using G.sumset_subset_carrier by blast
          have hB'ne: "?B'  {}" using hBne hbG ha1G sumset_is_empty_iff hBG by auto
          have hstabeq: "G.stabilizer (G.sumset A B) = G.stabilizer (G.sumset A ?B')" 
            using hbG ha1G hAG hBG G.stabilizer_unchanged by blast 
          have hstab0': "G.stabilizer (G.sumset A ?B') = {[𝟬]}" using hstab0 hstabeq by blast
          have ha1B': "a  ?B'"
          proof-
            have "(b [⊕] G.inverse b) [⊕] a  ?B'" using hBG hbG ha1G hb G.minusset.minussetI by blast
            thus "a  ?B'" by (simp add: hbG ha1G)
          qed
          then have hinter_nempty: "A  ?B'  {}" using ha1B' haA by blast
          have ha2B': "a'  ?B'" 
          proof-
            have h1: "(a' [⊕] b [⊕] G.inverse a) [⊕] G.inverse b  G.differenceset B {b}"
            proof
              assume "(a' [⊕] b [⊕] G.inverse a) [⊕] G.inverse b  G.differenceset B {b}"
              then obtain b' where "(a' [⊕] b [⊕] G.inverse a) [⊕] G.inverse b = b' [⊕] G.inverse b" 
                and "b'  B" using hbG G.minusset.simps G.sumset.cases by force
              then have "(a' [⊕] b [⊕] G.inverse a)  B" using hbG
                by (smt (verit) G.composition_closed hBG ha1G ha2G G.inverse_closed G.invertible 
                    G.invertible_right_cancel subsetD)
              thus "False" using habG by auto
            qed
            have "((a' [⊕] b [⊕] G.inverse a) [⊕] G.inverse b) [⊕] a  ?B'" 
            proof
              assume "((a' [⊕] b [⊕] G.inverse a) [⊕] G.inverse b) [⊕] a  ?B'"
              then obtain b' where "((a' [⊕] b [⊕] G.inverse a) [⊕] G.inverse b) [⊕] a = b' [⊕] a" 
                and "b'  G.differenceset B {b}" using ha1G G.sumset.simps by auto
              then have "((a' [⊕] b [⊕] G.inverse a) [⊕] G.inverse b)  G.differenceset B {b}" 
                using ha1G by (smt (z3) G.sumset.simps G.additive_abelian_group_axioms 
                    G.composition_closed ha2G hbG G.inverse_closed G.invertible G.invertible_right_cancel)
              thus "False" using h1 by auto
            qed
            thus "a'  ?B'" using ha1G hbG
              by (smt (verit, del_insts) G.associative G.commutative G.composition_closed ha2G 
                  G.inverse_closed G.invertible G.invertible_left_inverse G.right_unit)
          qed
          have hinterA: "A  ?B'  A" using haA ha2B' by auto
          have hintercard0: "0 < card (A  ?B')"   
            using hA hB hinter_nempty card_gt_0_iff by blast
          have hintercardA: "card (A  ?B') < card A" using hA hB hinterA card_mono
            by (simp add: psubsetI psubset_card_mono)
          have inj: "inj_on (λ x. x [⊕] G.inverse b [⊕] a) G" using inj_onI ha1G hb G.invertible 
              G.inverse_closed G.composition_closed by (smt (verit) G.invertible_right_cancel hbG)
          have 1: "card (G.sumset A B) = card (G.sumset A ?B')"
            using G.card_differenceset_singleton_mem_eq G.card_sumset_singleton_subset_eq hAG hB'G 
              ha1G hbG G.sumset_assoc G.sumset_commute G.sumset_subset_carrier
            by (smt (verit, del_insts))
          obtain C where hCconv: "G.convergent C A ?B'" and hCmin: " Y. Y  G.convergent_set A ?B' 
             card (G.stabilizer Y)  card (G.stabilizer C)" 
            using G.exists_convergent_min_stabilizer[of n A ?B']
              hindG hA hB' hAG hB'G hinter_nempty hAne hcardsum hintercardA 1 hGroupG by auto
          have hC: "C  G.sumset A ?B'" and hCne: "C  {}" and
            hCcard: "card C + card (G.stabilizer C)  
            card (A  ?B') + card (G.sumset (A  ?B') (G.stabilizer C))"
            using G.convergent_def hCconv by auto 
          then have hCfinite: "finite C" using hC G.finite_sumset hA hB'
            by (meson finite_subset)
          have htranslate: "card (G.sumset A {[𝟬]}) + card (G.sumset ?B' {[𝟬]}) - card {[𝟬]}  
            card (G.sumset A ?B')"
          proof(cases "G.stabilizer C = {[𝟬]}")
            case hCstab0: True
            have "card (G.sumset A {[𝟬]}) + card (G.sumset ?B' {[𝟬]}) - card {[𝟬]} = card A + card ?B' -
              card {[𝟬]}" using hAG hB'G G.card_minusset' by fastforce
            also have "... = card (A  ?B') + card (A  ?B') - card {[𝟬]}" 
              using hA hB' card_Un_Int by fastforce
            also have "... = card (A  ?B') + card (G.sumset (A  ?B') {[𝟬]}) - card {[𝟬]}"
              by (simp add: Int_absorb1 Int_commute hAG G.sumset_subset_carrier)
            also have "...  card C" using hCcard hCstab0 by auto
            also have "...  card (G.sumset A ?B')" 
            using hC card_mono G.finite_sumset hA hB' by metis
            finally show ?thesis by simp
          next
            case hCstab_ne0: False
            have hCG: "C  G" using hC by (meson subset_trans G.sumset_subset_carrier)
            then have hstabC: "finite (G.stabilizer C)" using G.stabilizer_finite hCne hC 
              G.finite_sumset hA hB' by (metis Nat.add_0_right add_leE card.infinite hCcard 
              hintercard0 le_0_eq not_gr0)
            then have hcardstabC_gt_1: "card (G.stabilizer C) > 1" using G.zero_mem_stabilizer
              hCstab_ne0 hCG by (metis card_1_singletonE card_gt_0_iff diffs0_imp_equal empty_iff 
              gr_zeroI insertE less_one zero_less_diff)
            have "G.sumset (G.stabilizer C) (G.sumset A ?B')  G.sumset A ?B'"
               using G.finite_sumset G.stabilizer_is_nonempty G.stabilizer_subset_group
               G.sumset_eq_sub_stabilizer G.sumset_subset_carrier hA hB' hCstab_ne0 hstab0'
               subset_singletonD by metis
            moreover have "card (G.sumset (G.stabilizer C) (G.sumset A ?B'))  card (G.sumset A ?B')"
              using G.card_le_sumset G.finite_sumset hA hB' hstabC
              by (meson hCG G.sumset_subset_carrier G.unit_closed G.zero_mem_stabilizer)
            ultimately have "¬ G.sumset (G.stabilizer C) (G.sumset A ?B')  G.sumset A ?B'"
              using G.finite_sumset hA hB' card_seteq by metis
            then obtain x where hx1: "x  G.sumset (G.stabilizer C) (G.sumset A ?B')" and 
              hx2: "x  G.sumset A ?B'" by auto
            then obtain a1 b1 c where "x = c [⊕] (a1 [⊕] b1)" and "c  G.stabilizer C" and 
              ha1A: "a1  A" and hb1B': "b1  ?B'" and ha1memG: "a1  G" and hb1memG: "b1  G" 
              by (metis (no_types, lifting) G.sumset.cases)
            then have hx: "x  G.sumset (G.stabilizer C) {a1 [⊕] b1}" 
              using hx1 by (meson G.composition_closed hAG hB'G insertI1 G.stabilizer_subset_group 
              subsetD G.sumset.sumsetI)
            then have hnotsubAB: "¬ G.sumset {a1 [⊕] b1} (G.stabilizer C)  G.sumset A ?B'" 
              using hx2 G.sumset_commute by auto
            let ?A1 = "A  (G.sumset {a1} (G.stabilizer C))"
            let ?A2 = "A  (G.sumset {b1} (G.stabilizer C))"
            let ?B1 = "?B'  (G.sumset {b1} (G.stabilizer C))"
            let ?B2 = "?B'  (G.sumset {a1} (G.stabilizer C))"
            let ?C1 = "C  (G.sumset ?A1 ?B1)"
            let ?C2 = "C  (G.sumset ?A2 ?B2)"
            let ?H1 = "G.stabilizer (G.sumset ?A1 ?B1)"
            let ?H2 = "G.stabilizer (G.sumset ?A2 ?B2)"
            have hA1ne: "?A1  {}" using ha1A G.zero_mem_stabilizer hCG
              by (metis (full_types) disjoint_iff_not_equal hAG insertCI G.right_unit subset_eq 
                G.sumset.sumsetI G.unit_closed)
            have hB1ne: "?B1  {}" using hb1B' G.zero_mem_stabilizer hCG
              by (metis G.composition_closed disjoint_iff_not_equal insertCI G.left_unit 
                  G.sumset.cases G.sumset.sumsetI G.sumset_commute G.unit_closed)
            have hnotsubC: "¬ G.sumset {a1 [⊕] b1} (G.stabilizer C)  C" using hnotsubAB hC by blast
            have habstabempty: "G.sumset {a1 [⊕] b1} (G.stabilizer C)  C = {}"
            proof(rule ccontr)
              assume "G.sumset {a1 [⊕] b1} (G.stabilizer C)  C  {}"
              then obtain z where 
                hz: "G.sumset {a1 [⊕] b1} (G.stabilizer C)  G.sumset {z} (G.stabilizer C)  {}" and 
                hzC: "z  C"   using G.stabilizer_coset_Un hCG by blast 
              then have "G.sumset {a1 [⊕] b1} (G.stabilizer C) = G.sumset {z} (G.stabilizer C)" using hz 
                G.sumset_stabilizer_eq_iff hCG G.sumset.simps hx by auto
              then have "G.sumset {a1 [⊕] b1} (G.stabilizer C)  C" using hzC 
                by (simp add: hCG G.stabilizer_coset_subset)
              thus "False" using hnotsubC by simp
            qed
            have hA1B1sub: "G.sumset ?A1 ?B1  G.sumset {a1 [⊕] b1} (G.stabilizer C)" and 
              hB2A2sub: "G.sumset ?B2 ?A2  G.sumset {a1 [⊕] b1} (G.stabilizer C)"
              using G.sumset_Inter_subset_sumset ha1memG hb1memG by auto
            then have hA1B1Cempty: "G.sumset ?A1 ?B1  C = {}" using habstabempty by blast
            then have hcardC1: "card ?C1 = card C + card (G.sumset ?A1 ?B1)" using card_Un_disjoint 
              G.finite_sumset hA hB' finite_Int hC finite_subset Int_commute by metis
            have hA1B1cardless: "card (G.sumset ?A1 ?B1) < card (G.sumset A B)"
            proof-
              have "G.sumset ?A1 ?B1  G.sumset A ?B'" using G.sumset_mono by auto
              moreover have "G.sumset ?A1 ?B1  G.sumset A ?B'" 
                using hA1B1Cempty hC hCne hA1B1sub by auto
              ultimately show "card (G.sumset ?A1 ?B1) < card (G.sumset A B)" 
                  using G.finite_sumset hA hB' psubset_card_mono psubset_eq 1 by metis
            qed
            have hB2A2Cempty: "G.sumset ?B2 ?A2  C = {}" using habstabempty hB2A2sub by blast
            then have hcardC2: "card ?C2 = card C + card (G.sumset ?B2 ?A2)" using card_Un_disjoint 
              G.finite_sumset hA hB' finite_Int hC finite_subset Int_commute G.sumset_commute by metis
            have hA2B2cardless: "card (G.sumset ?A2 ?B2) < card (G.sumset A B)"
            proof-
              have "G.sumset ?A2 ?B2  G.sumset A ?B'" 
                using G.sumset_mono hB2A2Cempty hC hCne hB2A2sub G.sumset_commute psubset_eq
                by (metis Int_absorb1 Int_lower1)
              then show ?thesis by (simp add: 1 G.finite_sumset hA hB' psubset_card_mono)
            qed
            have "card ?A1  card A" using card_mono hA by (metis Int_lower1)
            then have "card (G.sumset ?A1 ?B1) + card ?A1 < card (G.sumset A B) + card A" 
              using hA1B1cardless by linarith
            then obtain l where hln: "l < n" and hind1: "card (G.sumset ?A1 ?B1) + card ?A1 = l" 
              using hcardsum by auto
            have "card ?A2  card A" using card_mono hA Int_lower1 by metis
            then have "card (G.sumset ?A2 ?B2) + card ?A2 < card (G.sumset A B) + card A"
              using hA2B2cardless by linarith
            then obtain k where hkn: "k < n" and hind2: "card (G.sumset ?A2 ?B2) + card ?A2 = k"
                using hcardsum by auto
            have hH1stabC: "?H1  G.stabilizer C" using G.stabilizer_sumset_psubset_stabilizer 
                hA1ne hB1ne ha1memG hb1memG hnotsubAB by presburger
            then have "card ?H1 < card (G.stabilizer C)" using psubset_card_mono hstabC by auto
            moreover have hC1H1: "?H1 = G.stabilizer ?C1" using G.stabilizer_eq_stabilizer_union
              by (metis Int_commute hA hA1B1Cempty hA1ne hB' hB1ne hC hCfinite hCne ha1memG hb1memG hnotsubAB)
            ultimately have hC1notconv: "¬ G.convergent ?C1 A ?B'" using hCmin G.convergent_set_def
              le_antisym less_imp_le_nat less_not_refl2 by fastforce
            have hC1ne: "?C1  {}" and hC2ne: "?C2  {}" using hCne by auto
            have hC1AB': "?C1  G.sumset A ?B'" and hC2AB': "?C2  G.sumset A ?B'" using hC 
              by (auto simp add: G.sumset_mono)
            have hA1G: "?A1  G" and hA1 : "finite ?A1" and hB1G: "?B1  G" and hB1: "finite ?B1" 
              using hAG hB'G hA hB' finite_Int by auto
            then have hindA1B1: "card (G.sumset ?A1 ?H1) + card (G.sumset ?B1 ?H1) - card ?H1  
              card (G.sumset ?A1 ?B1)" using hindG hGroupG hA1ne hB1ne hind1 hln hAG hB'G 
              hA hB' by metis
            have hC1notconv_ineq: 
              "(int (card ?C1) + card ?H1 - card (A  ?B')) < int (card (G.sumset (A  ?B') ?H1))" 
              using hC1notconv hC1ne hC1AB' hC1H1 G.convergent_def by auto
            have "int (card (G.sumset (A  ?B') (G.stabilizer C))) - card (G.sumset (A  ?B') ?H1)
             (int (card C) + card (G.stabilizer C) - card (A  ?B')) - card (G.sumset (A  ?B') ?H1)" 
            using hCcard by linarith
            then have "int (card (G.sumset (A  ?B') (G.stabilizer C))) - card (G.sumset (A  ?B') ?H1) <
              (int (card C) + card (G.stabilizer C) - card (A  ?B')) - 
              (int (card ?C1) + card ?H1 - card (A  ?B'))" using hC1notconv_ineq by linarith
            also have "... = int (card (G.stabilizer C)) - card ?H1 - card (G.sumset ?A1 ?B1)" 
              using hcardC1 by presburger
            also have "...  int (card (G.stabilizer C)) - card (G.sumset ?A1 ?H1) - card (G.sumset ?B1 ?H1)"
              using hindA1B1 by linarith
            text‹ Finally, we deduce the inequality that is referred to as
     inequality (1) in \cite{DeVos_Kneser} for @{term ?A1} and  @{term ?B1}. ›
            finally have hA1B1ineq: "int (card (G.sumset (A  ?B') (G.stabilizer C))) - 
              card (G.sumset (A  ?B') ?H1) < int (card (G.stabilizer C)) - 
              card (G.sumset ?A1 ?H1) - card (G.sumset ?B1 ?H1)" by simp
            have hB2ne: "?B2  {}" using G.sumset_inter_ineq hA1B1ineq ha1A ha1G hA hB' hAne hB'ne 
              hstabC hH1stabC ha1memG of_nat_0_le_iff by (smt (verit, del_insts))
            have hA2ne: "?A2  {}" using G.sumset_inter_ineq[of "A" "b1" "C" "?B'" "a1"] hA1B1ineq 
              hb1B' hb1memG hA hB' hAne hB'ne  hstabC hH1stabC of_nat_0_le_iff G.sumset_commute Un_commute by (smt (verit, ccfv_SIG))
            have hH2stabC: "?H2  G.stabilizer C" using G.stabilizer_sumset_psubset_stabilizer 
              G.commutative hA2ne hB2ne ha1memG hb1memG hnotsubAB by presburger
            then have "card ?H2 < card (G.stabilizer C)" using psubset_card_mono hstabC by auto
            moreover have hC2H2: "?H2 = G.stabilizer ?C2" using G.stabilizer_eq_stabilizer_union
              by (smt (verit, ccfv_threshold) G.sumset_commute Int_commute hA hA2ne hB' hB2A2Cempty
                hB2ne hC hCfinite hCne ha1memG hb1memG hnotsubAB)
            ultimately have hC2notconv: "¬ G.convergent ?C2 A ?B'" 
              using hCmin G.convergent_set_def le_antisym less_imp_le_nat less_not_refl2 
              by fastforce
            have hA2G: "?A2  G" and hA2 : "finite ?A2" and hB2G: "?B2  G" and hB2: "finite ?B2" 
              using hAG hB'G hA hB' finite_Int by auto
            then have hindA2B2: "card (G.sumset ?A2 ?H2) + card (G.sumset ?B2 ?H2) - card ?H2  
              card (G.sumset ?A2 ?B2)"
              using hindG hGroupG hA2ne hB2ne hind2 hkn hAG hB'G hA hB' by metis
            have hC2notconv_ineq: 
              "(int (card ?C2) + card ?H2 - card (A  ?B')) < int (card (G.sumset (A  ?B') ?H2))" 
              using hC2notconv hC2ne hC2AB' hC2H2 G.convergent_def by auto
            have "int (card (G.sumset (A  ?B') (G.stabilizer C))) - card (G.sumset (A  ?B') ?H2)
               (int (card C) + card (G.stabilizer C) - card (A  ?B')) - card (G.sumset (A  ?B') ?H2)" 
              using hCcard by linarith
            then have "int (card (G.sumset (A  ?B') (G.stabilizer C))) - card (G.sumset (A  ?B') ?H2) <
              (int (card C) + card (G.stabilizer C) - card (A  ?B')) - 
              (int (card ?C2) + card ?H2 - card (A  ?B'))" using hC2notconv_ineq by linarith
            also have "... = int (card (G.stabilizer C)) - card ?H2 - card (G.sumset ?A2 ?B2)" 
              using hcardC2 G.sumset_commute by simp
            also have "...  int (card (G.stabilizer C)) - card (G.sumset ?A2 ?H2) - card (G.sumset ?B2 ?H2)"
              using hindA2B2 by linarith
            
            text‹ Analogously, we deduce the inequality that is referred to as
     inequality (1) in \cite{DeVos_Kneser} for @{term ?A2} and  @{term ?B2}. ›
           
            finally have hA2B2ineq: "int (card (G.sumset (A  ?B') (G.stabilizer C))) - 
              card (G.sumset (A  ?B') ?H2) < int (card (G.stabilizer C)) - 
              card (G.sumset ?A2 ?H2) - card (G.sumset ?B2 ?H2)" by simp
            have hfinsumH2:"finite (G.sumset (A  ?B') ?H2)" 
              using G.finite_sumset hA hB' finite_UnI hstabC hH2stabC finite_subset psubset_imp_subset
              by metis
            have hsubsumH2: "G.sumset (A  ?B') ?H2  G.sumset (A  ?B') (G.stabilizer C)" 
              using G.sumset.cases hAG hB'G G.stabilizer_subset_group hH2stabC psubset_imp_subset
              by (smt (verit, best) subset_Un_eq G.sumset_commute G.sumset_subset_Un1)
            then have hsumH2card_le: "card (G.sumset (A  ?B') ?H2)  
              card (G.sumset (A  ?B') (G.stabilizer C))"
              using card_mono G.finite_sumset G.stabilizer_finite hC hCne hCG hA hB'
              by (metis finite_UnI hstabC)
            have hfinsumH1: "finite (G.sumset (A  ?B') ?H1)" 
              using finite_sumset finite_Un psubsetE by (metis G.finite_sumset G.stabilizer_finite 
                G.sumset_subset_carrier Int_Un_eq(4) hA hA1 hB' hB1 hC1H1 hH1stabC habstabempty)
            have hsubsumH1: "G.sumset (A  ?B') ?H1  G.sumset (A  ?B') (G.stabilizer C)" 
              using G.sumset.cases psubsetE subset_refl G.sumset_mono hH1stabC by simp
            have hsumH1card_le: "card (G.sumset (A  ?B') ?H1)  card (G.sumset (A  ?B') (G.stabilizer C))"
              using card_mono G.finite_sumset G.stabilizer_finite by (metis finite_UnI hA hB' hstabC hsubsumH1)
            have ha1b1stabCne: "G.sumset {a1} (G.stabilizer C)  G.sumset {b1} (G.stabilizer C)"
            proof
              assume ha1b1: "G.sumset {a1} (G.stabilizer C) = G.sumset {b1} (G.stabilizer C)"
              have hfin: "finite (G.sumset ?A1 ?H1  G.sumset ?B1 ?H1)" 
                using finite_UnI G.finite_sumset hA1 hB1 hH1stabC hstabC psubset_imp_subset
                by (metis finite_subset)
              have "int (card (G.sumset {a1} (G.stabilizer C))) - card (G.sumset ?A1 ?H1) - 
                card (G.sumset ?B1 ?H1)  int (card (G.sumset {a1} (G.stabilizer C))) - 
                card (G.sumset ?A1 ?H1  G.sumset ?B1 ?H1)"
                using card_Un_le[of "G.sumset ?A1 ?H1" "G.sumset ?B1 ?H1"] by linarith
              also have "...  card (G.sumset {a1} (G.stabilizer C) - (G.sumset ?A1 ?H1  G.sumset ?B1 ?H1))"
                using diff_card_le_card_Diff[of "G.sumset ?A1 ?H1  G.sumset ?B1 ?H1" 
                  "G.sumset {a1} (G.stabilizer C)"] hfin by linarith
              also have "...  card (G.sumset {a1} (G.stabilizer C) - G.sumset (?A1  ?B1) ?H1)"
                using G.sumset_subset_Un1 by auto
              also have "...  card (G.sumset (A  ?B') (G.stabilizer C) - G.sumset (A  ?B') ?H1)"
              proof-
                have hsub: "G.sumset {a1} (G.stabilizer C) - G.sumset (?A1  ?B1) ?H1  
                  G.sumset (A  ?B') (G.stabilizer C) - G.sumset (A  ?B') ?H1"
                proof
                  fix x assume hx: "x  G.sumset {a1} (G.stabilizer C) - G.sumset (?A1  ?B1) ?H1"
                  then obtain c where hxac: "x = a1 [⊕] c" and hc: "c  G.stabilizer C" 
                    using G.sumset.cases by blast
                  then have "x  G.sumset (A  ?B') (G.stabilizer C)" using ha1A hAG 
                    G.stabilizer_subset_group by (simp add: subset_iff G.sumset.sumsetI)
                  moreover have "x  G.sumset (A  ?B') ?H1"
                  proof
                    assume hx1: "x  G.sumset (A  ?B') ?H1"
                    then obtain y h1 where hxy: "x = y [⊕] h1" and hy: "y  A  ?B'" and 
                      hh1: "h1  ?H1" using G.sumset.cases by blast
                    then have hyG: "y  G" and hcG: "c  G" and hh1G: "h1  G" 
                      using hAG hB'G G.stabilizer_subset_group hc by auto
                    then have "y = a1 [⊕] (c [⊕] G.inverse h1)" using hxac hxy ha1A hAG 
                      by (metis G.associative G.commutative G.composition_closed in_mono 
                        G.inverse_closed G.invertible G.invertible_left_inverse2)
                    moreover have "h1  G.stabilizer C" using hh1 hH1stabC by auto
                    moreover hence "c [⊕] G.inverse h1  G.stabilizer C" using hc
                        G.stabilizer_is_subgroup subgroup_def G.group_axioms
                        group.invertible subgroup.subgroup_inverse_iff 
                        submonoid.sub_composition_closed hh1G by metis
                    ultimately have "y  G.sumset {a1} (G.stabilizer C)" using ha1G hcG hAG ha1A hh1G
                      by blast
                    then have "y  ?A1  ?B1" using hy  by (simp add: ha1b1)
                    thus "False" using hx hxy hh1 hh1G hyG by auto
                  qed
                  ultimately show "x  G.sumset (A  ?B') (G.stabilizer C) - G.sumset (A  ?B') ?H1" by simp
                qed
                moreover have "finite (G.sumset {a1} (G.stabilizer C) - G.sumset (?A1  ?B1) ?H1)"
                  using finite_subset G.finite_sumset hstabC by simp
                moreover hence "finite (G.sumset (A  ?B') (G.stabilizer C) - G.sumset (A  ?B') ?H1)"
                  using finite_subset G.finite_sumset hstabC hA hB' finite_UnI by simp
                moreover have "card (G.sumset {a1} (G.stabilizer C) - G.sumset (?A1  ?B1) ?H1)  
                  card (G.sumset (A  ?B') (G.stabilizer C) - G.sumset (A  ?B') ?H1)" 
                  using card_mono hsub calculation(3) by auto
                ultimately show ?thesis using card_Diff_subset by linarith
              qed
              also have "... = int (card (G.sumset (A  ?B') (G.stabilizer C))) - card (G.sumset (A  ?B') ?H1)"
                using card_Diff_subset[OF hfinsumH1 hsubsumH1] hsumH1card_le by linarith
              finally have "int (card (G.stabilizer C)) - card (G.sumset ?A1 ?H1) - card (G.sumset ?B1 ?H1)
                 int (card (G.sumset (A  ?B') (G.stabilizer C))) - card (G.sumset (A  ?B') ?H1)"
                using hCG subset_iff G.card_sumset_singleton_subset_eq G.stabilizer_subset_group 
                hAG ha1A by auto
              thus "False" using hA1B1ineq by linarith
            qed
            have "int (card (G.sumset (A  ?B') (G.stabilizer C))) - 
              card (G.sumset (A  ?B') ?H1)  0" by (simp add: hsumH1card_le)
            then have "int (card (G.stabilizer C)) - 
              card (G.sumset ?A1 ?H1) - card (G.sumset ?B1 ?H1) > 0" using hA1B1ineq by linarith
            moreover have "int (card ?H1) dvd int (card (G.stabilizer C)) - 
              card (G.sumset ?A1 ?H1) - card (G.sumset ?B1 ?H1)" using 
              G.stabilizer_subset_stabilizer_dvd hH1stabC psubset_imp_subset int_dvd_int_iff dvd_diff
              G.card_stabilizer_divide_sumset[OF hA1G] G.card_stabilizer_divide_sumset[OF hB1G]
              by fastforce
            ultimately have "int (card (G.stabilizer C)) - 
              card (G.sumset ?A1 ?H1) - card (G.sumset ?B1 ?H1)  int (card ?H1)" 
              using zdvd_imp_le by blast
            moreover have hA1_le_sum: "card ?A1  card (G.sumset ?A1 ?H1)"
              using G.sumset_commute G.card_le_sumset G.zero_mem_stabilizer hA1G hA1 hH1stabC hstabC 
              by (metis finite_subset psubset_imp_subset G.unit_closed)
            moreover have hB1_le_sum: "card ?B1  card (G.sumset ?B1 ?H1)"
              using G.sumset_commute G.card_le_sumset G.zero_mem_stabilizer hB1G hB1 hH1stabC hstabC 
              by (metis finite_subset psubset_imp_subset G.unit_closed)
            
            text‹ The above facts combined allow us to deduce the inequality that is referred to as
     inequality (2) in  \cite{DeVos_Kneser} for @{term ?A1},  @{term ?B1} and @{term ?H1}. ›
           
            ultimately have 21: "int (card (G.stabilizer C))  int (card ?H1) + card ?A1 + card ?B1" 
              by linarith
            have "int (card (G.sumset (A  ?B') (G.stabilizer C))) - 
              card (G.sumset (A  ?B') ?H2)  0" by (simp add: hsumH2card_le)
            then have "int (card (G.stabilizer C)) - 
              card (G.sumset ?A2 ?H2) - card (G.sumset ?B2 ?H2) > 0" using hA2B2ineq by linarith
            moreover have "int (card ?H2) dvd int (card (G.stabilizer C)) - 
              card (G.sumset ?A2 ?H2) - card (G.sumset ?B2 ?H2)" using psubset_imp_subset
              G.stabilizer_subset_stabilizer_dvd hH2stabC int_dvd_int_iff dvd_diff
              G.card_stabilizer_divide_sumset[OF hA2G] G.card_stabilizer_divide_sumset[OF hB2G] 
              by fastforce
            ultimately have "int (card (G.stabilizer C)) - 
              card (G.sumset ?A2 ?H2) - card (G.sumset ?B2 ?H2)  int (card ?H2)" 
              using zdvd_imp_le by blast
            moreover have hA2_le_sum: "card ?A2  card (G.sumset ?A2 ?H2)"
              using G.sumset_commute G.card_le_sumset G.zero_mem_stabilizer G.stabilizer_subset_group 
                hA2G hA2 hH2stabC hstabC psubset_imp_subset by (metis finite_subset G.unit_closed)
            moreover have hB2_le_sum: "card ?B2  card (G.sumset ?B2 ?H2)"
              using G.sumset_commute G.card_le_sumset G.zero_mem_stabilizer G.stabilizer_subset_group 
                hB2G hB2 hH2stabC hstabC psubset_imp_subset by (metis finite_subset G.unit_closed)
     
 text‹Analogously, the above facts combined allow us to deduce the inequality that is referred to as
     inequality (2) in \cite{DeVos_Kneser} for @{term ?A2},  @{term ?B2} and @{term ?H2}. ›

            ultimately have 22: "int (card (G.stabilizer C))  int (card ?H2) + card ?A2 + card ?B2" 
              by linarith
            let ?S = "G.sumset {a1} (G.stabilizer C) - (?A1  ?B2)"
            let ?T = "G.sumset {b1} (G.stabilizer C) - (?A2  ?B1)"
            have hS : "finite ?S" and hT: "finite ?T" using G.finite_sumset hstabC by auto
            have hST: "?S  ?T = {}" using ha1b1stabCne Diff_Int2 Diff_Int_distrib2 Int_Diff Int_Un_eq(4) 
              Int_absorb Int_commute Int_empty_right Int_insert_right Un_empty empty_Diff hA1ne 
              hA2ne G.sumset_commute G.sumset_is_empty_iff G.sumset_stabilizer_eq_iff
              by (smt (verit, ccfv_threshold) G.sumset_assoc)
            have hSTcard_le: "card ?S + card ?T + card (G.sumset (A  ?B') {[𝟬]})  
                card (G.sumset (A  ?B') (G.stabilizer C))" 
            proof-
              have "G.sumset {a1} (G.stabilizer C)  G.sumset (A  ?B') (G.stabilizer C)" and 
                "G.sumset {b1} (G.stabilizer C)  G.sumset (A  ?B') (G.stabilizer C)" 
                using G.sumset_mono ha1A hb1B' subset_refl empty_subsetI insert_subset by auto
              moreover have "(G.sumset (A  ?B') {[𝟬]})  G.sumset (A  ?B') (G.stabilizer C)"
                using G.sumset_mono subset_refl empty_subsetI insert_subset G.zero_mem_stabilizer 
                by metis
              ultimately have hsub: "?S  ?T  (G.sumset (A  ?B') {[𝟬]})  
                G.sumset (A  ?B') (G.stabilizer C)" by blast
              have "?S  G.sumset (A  ?B') {[𝟬]} = {}" by auto
              moreover have "(?S  ?T)  G.sumset (A  ?B') {[𝟬]} = {}" by auto
              ultimately have "card ?S + card ?T + card (G.sumset (A  ?B') {[𝟬]}) = 
                card (?S  ?T  (G.sumset (A  ?B') {[𝟬]}))" using card_Un_disjoint hS hT 
                G.finite_sumset finite_UnI hA hB' hST by (metis finite.emptyI finite.insertI)
              also have "...  card (G.sumset (A  ?B') (G.stabilizer C))" using card_mono 
                G.finite_sumset finite_UnI hA hB' hstabC hsub by metis 
              finally show ?thesis by simp
            qed
            have hAB_not_conv: "¬ G.convergent (G.sumset A ?B') A ?B'" using hCmin hstab0 
                G.convergent_set_def hcardstabC_gt_1 hstab0' by fastforce
            then have "card (G.sumset A ?B') + card {[𝟬]} < card (A  ?B') + 
              card (G.sumset (A  ?B') {[𝟬]})" using G.convergent_def hAne hB'ne hAG hB'G hstab0' 
              subset_refl by auto
            then have hAB'sum: "int (card (G.sumset (A  ?B') {[𝟬]})) + card (A  ?B') - 
              card (G.sumset A ?B') > 1" by simp
            moreover have "int (card ?A1) + card ?B1  int (card (G.sumset ?A1 ?H1)) + 
              card (G.sumset ?B1 ?H1)" using hA1_le_sum hB1_le_sum by linarith
            moreover hence "int (card ?A1) + card ?B1 - card ?H1  card (G.sumset ?A1 ?B1)" 
              using hindA1B1 by linarith
            ultimately have "int (card ?S) + card ?T + card ?A1 + card ?B1 - card ?H1 < 
              int (card ?S) + card ?T + card (G.sumset (A  ?B') {[𝟬]}) + card (A  ?B') - 
              card (G.sumset A ?B') + card (G.sumset ?A1 ?B1)" by linarith
            also have "...  int (card (G.sumset (A  ?B') (G.stabilizer C))) + card (A  ?B') - card C"
            proof-
              have "G.sumset ?A1 ?B1  C  G.sumset A ?B'" using hC G.sumset_mono by auto
              then have "card (G.sumset ?A1 ?B1) + card C  
                card (G.sumset A ?B')" using card_Un_disjoint hCfinite G.finite_sumset hA1 hB1 hA1B1Cempty 
                  card_mono hA hB' by metis
              then show ?thesis using hSTcard_le by linarith
            qed

            text‹From this, inequality (3) \cite{DeVos_Kneser} follows for @{term ?A1},  
            @{term ?B1} and @{term ?H1}.›

            finally have 31: "int (card ?S) + card ?T + card ?A1 + card ?B1 - card ?H1 < 
              card (G.stabilizer C)" using hCcard by linarith
            have "int (card ?A2) + card ?B2  int (card (G.sumset ?A2 ?H2)) + 
              card (G.sumset ?B2 ?H2)" using hA2_le_sum hB2_le_sum by linarith
            moreover hence "int (card ?A2) + card ?B2 - card ?H2  card (G.sumset ?A2 ?B2)" 
              using hindA2B2 by linarith
            ultimately have "int (card ?S) + card ?T + card ?A2 + card ?B2 - card ?H2 < 
              int (card ?S) + card ?T + card (G.sumset (A  ?B') {[𝟬]}) + card (A  ?B') - 
              card (G.sumset A ?B') + card (G.sumset ?A2 ?B2)" using hAB'sum by linarith
            also have "...  int (card (G.sumset (A  ?B') (G.stabilizer C))) + card (A  ?B') - card C"
            proof-
              have "G.sumset ?A2 ?B2  C  G.sumset A ?B'" using hC G.sumset_mono by auto
              then have "card (G.sumset ?A2 ?B2) + card C  
                card (G.sumset A ?B')" using card_Un_disjoint hCfinite G.finite_sumset hA2 hB2 hA1B1Cempty 
                  card_mono hA hB' hB2A2Cempty G.sumset_commute by metis
              then show ?thesis using hSTcard_le by linarith
            qed
 
            text‹From this, inequality (3) \cite{DeVos_Kneser} follows for @{term ?A2},
            @{term ?B2} and @{term ?H2}.›

            finally have 32: "int (card ?S) + card ?T + card ?A2 + card ?B2 - card ?H2 < 
              card (G.stabilizer C)" using hCcard by linarith
            
            text‹ Adding together the four inequalities obtained by versions of inequalities
               (2) and (3) and dividing by 2 gives the following inequality: › 
            
            have 4: "2 * int (card (G.stabilizer C)) > int (card ?A1) + card ?B2 + card ?S + card ?T + card ?B1 + card ?A2"
              using 21 22 31 32 by linarith
            have "G.sumset {a1} (G.stabilizer C) = (?S  ?A1)  ?B2" and
              hb1T: "G.sumset {b1} (G.stabilizer C) = (?T  ?A2)  ?B1" by auto
            then have "card (G.stabilizer C)  card ?S + card ?A1 + card ?B2"
              using card_Un_le[of "?S" "?A1"] card_Un_le[of "?S  ?A1" "?B2"] 
                G.card_sumset_singleton_subset_eq G.stabilizer_subset_group ha1A hAG by auto
            moreover have "card (G.stabilizer C)  card ?T + card ?A2 + card ?B1"
              using hb1T card_Un_le[of "?T" "?A2"] card_Un_le[of "?T  ?A2" "?B1"]
              G.card_sumset_singleton_subset_eq G.stabilizer_subset_group hb1B' hB'G by auto
            
            text‹ Combining the inequality labelled @{term 4} above with the above facts, the claim 
     follows:›
            ultimately show ?thesis using 4 by linarith
          qed
   
          text‹It remains to transfer the statement of inequality labelled @{term 1} into an analogous 
       one, which replaces @{term ?B'} with @{term B}. ›

          have 2: "card (G.sumset A (G.stabilizer (G.sumset A B))) = 
            card (G.sumset A (G.stabilizer (G.sumset A ?B')))"
            using hstabeq by auto
          have 3: "card (G.sumset B (G.stabilizer (G.sumset A B))) = 
            card (G.sumset ?B' (G.stabilizer (G.sumset A ?B')))" using hstabeq hstab0' G.sumset_commute
            by (metis G.card_differenceset_singleton_mem_eq G.card_sumset_singleton_subset_eq 
            G.sumset_D(1) G.sumset_commute G.sumset_subset_carrier Int_absorb1 Int_commute hBG ha1G hbG)
          then show ?thesis using 1 2 3 hstabeq hstab0' htranslate by auto
        qed
      next
        case hstabne0: False
        let ?K = "G.stabilizer (G.sumset A B)"
        have hcardK_gt_1: "card ?K > 1" using G.stabilizer_finite G.sumset_subset_carrier G.finite_sumset 
          hA hB hstabne0 G.zero_mem_stabilizer by (metis card_0_eq card_1_singletonE G.card_sumset_0_iff 
          empty_iff hAG hAne hBG hBne insertE less_one linorder_neqE_nat)
        interpret K: subgroup_of_additive_abelian_group ?K G "([⊕])" "[𝟬]"
          using G.stabilizer_is_subgroup subgroup_of_additive_abelian_group_def 
          by (metis G.abelian_group_axioms G.group_axioms hGroupG subgroup_of_abelian_group_def 
            subgroup_of_group.intro)
        let  = "K.Class"
        have : " a. a  G   a = (λ x. G.sumset {x} ?K) a" 
          using K.Left_Coset_Class_unit G.Left_Coset_eq_sumset_stabilizer by simp
        interpret GK: additive_abelian_group "G.Factor_Group G ?K" K.quotient_composition "K.Class [𝟬]"
        proof
          fix x y assume "x  K.Partition" and "y  K.Partition"
          then obtain a b where "x = K.Class a" and "y = K.Class b" and "a  G" and "b  G" 
            by (meson K.representant_exists)
          then show "K.quotient_composition x y = K.quotient_composition y x"
            using K.Class_commutes_with_composition G.commutative by presburger
        qed
        have hGroupGK: "additive_abelian_group (G.Factor_Group G ?K) K.quotient_composition (K.Class [𝟬])" ..
        
        text‹Here, we specialize the induction hypothesis to the factor group.›

        let ?K_repr = "K.φ ` K.Partition"
        have " x y. x  ?K_repr  y  ?K_repr  K.quot_comp_alt x y = K.quot_comp_alt y x"
          using K.quot_comp_alt_def G.commutative K.phi_image_subset subsetD by (metis (full_types))
        then interpret K_repr: additive_abelian_group ?K_repr K.quot_comp_alt "K.φ ?K"
          using Group_Theory.group.axioms(1)[OF K.phi_image_group]
          by (auto simp add: additive_abelian_group_def abelian_group_def K.phi_image_group
            commutative_monoid_axioms_def commutative_monoid_def)
        have hindrepr: " m C D. m < n  C  ?K_repr  D  ?K_repr  finite C 
          finite D  C  {}  D  {}  card (K_repr.sumset C D) + card C = m  
          card (K_repr.sumset C (K_repr.stabilizer (K_repr.sumset C D))) + 
          card (K_repr.sumset D (K_repr.stabilizer (K_repr.sumset C D))) - card (K_repr.stabilizer (K_repr.sumset C D)) 
          card (K_repr.sumset C D)" using hind K_repr.additive_abelian_group_axioms by blast
        have hindfactor: " m C D. m < n   C  K.Partition  D  K.Partition  finite C 
          finite D  C  {}  D  {}  card (GK.sumset C D) + card C = m  
          card (GK.sumset C (GK.stabilizer (GK.sumset C D))) + 
          card (GK.sumset D (GK.stabilizer (GK.sumset C D))) - card (GK.stabilizer (GK.sumset C D)) 
          card (GK.sumset C D)"
        proof(intro impI)
          fix m C D assume hmn: "m < n" and hCK: "C  K.Partition" and hDK: "D  K.Partition" and 
          hC: "finite C" and hD: "finite D" and hCne: "C  {}" and hDne: "D  {}" and 
          hCDcard: "card (GK.sumset C D) + card C = m"
          let ?C = "K.φ ` C" and ?D = "K.φ ` D"
          have hCrepr: "?C  ?K_repr" and hDrepr: "?D  ?K_repr" using hCK hDK by auto
          have hCfin: "finite ?C" and hDfin: "finite ?D" and hCne_1: "?C  {}" and hDne_1: "?D  {}" using hC hD hCne hDne by auto
          have hcardC: "card ?C = card C" using K.phi_inj_on hC card_image inj_on_subset hCK by metis
          have "card (GK.sumset C D) = card (K_repr.sumset ?C ?D)" 
            using card_image K.phi_inj_on inj_on_subset K.phi_image_sumset_eq 
              GK.sumset_subset_carrier hCK hDK by (smt (verit, best))
          then have "card (K_repr.sumset ?C ?D) + card ?C = m" using hCDcard hcardC by presburger
          then have "card (K_repr.sumset ?C (K_repr.stabilizer (K_repr.sumset ?C ?D))) + 
          card (K_repr.sumset ?D (K_repr.stabilizer (K_repr.sumset ?C ?D))) - card (K_repr.stabilizer (K_repr.sumset ?C ?D)) 
          card (K_repr.sumset ?C ?D)" 
            using hindrepr hCfin hDfin hCne_1 hDne_1 hCrepr hDrepr hmn by blast
          then show "card (GK.sumset C (GK.stabilizer (GK.sumset C D))) + 
          card (GK.sumset D (GK.stabilizer (GK.sumset C D))) - card (GK.stabilizer (GK.sumset C D)) 
          card (GK.sumset C D)" using K.phi_image_sumset_eq K.phi_image_stabilizer_eq
            K.phi_inj_on inj_on_subset hCK hDK card_image
            by (smt (z3) GK.stabilizer_subset_group GK.sumset_subset_carrier)
        qed
        have hstab0: "GK.stabilizer ( ` (G.sumset A B)) = {K.Class [𝟬]}"
        proof
          show "GK.stabilizer ( ` G.sumset A B)  {K.Class [𝟬]}"
          proof
            fix x assume hx: "x  GK.stabilizer ( ` G.sumset A B)"
            moreover have " ` G.sumset A B  K.Partition" 
              using K.natural.map_closed G.sumset_subset_carrier by blast
            ultimately have hsum: "GK.sumset {x} ( ` G.sumset A B) =  ` G.sumset A B" 
              using GK.stabilizer_def by auto
            obtain x' where hxφ: "x =  x'" and hx'G: "x'  G" 
              using hx GK.stabilizer_subset_group K.representant_exists by force
            have hsumset: "GK.sumset {x} ( ` G.sumset A B) = (λ a.  (x' [⊕] a)) ` G.sumset A B"
            proof
              show "GK.sumset {x} ( ` G.sumset A B)  (λa.  (x' [⊕] a)) ` G.sumset A B"
              proof
                fix y assume "y  GK.sumset {x} ( ` G.sumset A B)"
                then obtain z where "z  G.sumset A B" and "y = K.quotient_composition ( x') ( z)" 
                  using GK.sumset.cases hxφ by blast
                then show "y  (λa.  (x' [⊕] a)) ` G.sumset A B" 
                  using K.Class_commutes_with_composition G.composition_closed hx'G G.sumset.cases 
                    imageI by metis
              qed
            next
              show "(λa.  (x' [⊕] a)) ` G.sumset A B  GK.sumset {x} ( ` G.sumset A B)"
              proof
                fix y assume "y  (λa.  (x' [⊕] a)) ` G.sumset A B"
                then obtain z where hz: "z  G.sumset A B" and "y =  (x' [⊕] z)" by blast
                then have "y = K.quotient_composition ( x') ( z)" using 
                    K.Class_commutes_with_composition G.composition_closed hx'G G.sumset.cases by metis
                then show "y  GK.sumset {x} ( ` G.sumset A B)" 
                  using hxφ hz imageI hx GK.sumset.sumsetI K.natural.map_closed 
                  by (metis G.composition_closed hx'G insertCI G.sumset.cases)
              qed
            qed
            have "G.sumset {x'} (G.sumset A B)  G.sumset (G.sumset A B) ?K"
            proof
              fix y assume "y  G.sumset {x'} (G.sumset A B)"
              then obtain z where hz: "z  G.sumset A B" and hy: "y = x' [⊕] z" using G.sumset.cases by blast
              then have " (x' [⊕] z)   ` G.sumset A B" using hsum hsumset by blast
              then obtain w where hw: "{w}  G.sumset A B" and "w  G.sumset A B" 
                and " (x' [⊕] z) =  w" by auto
              then have "(x' [⊕] z)  G.differenceset (G.sumset {w} ?K) ?K" 
                using  G.sumset_subset_carrier hx'G hz G.sumset_eq_subset_differenceset 
                  G.composition_closed G.stabilizer_is_nonempty G.stabilizer_subset_group G.sumset.cases 
                   K.Class_self G.differenceset_stabilizer_eq G.sumset_assoc by metis
              moreover have "G.differenceset (G.sumset {w} ?K) ?K  G.sumset {w} ?K" 
                using hw by (simp add: G.differenceset_stabilizer_eq G.sumset_assoc)
              ultimately show "y  G.sumset (G.sumset A B) ?K" using hy hw G.sumset_mono subsetD 
                subset_refl by blast
            qed
            moreover have "G.sumset (G.sumset A B) ?K = G.sumset A B" 
              using G.sumset_commute G.sumset_stabilizer_eq_self G.sumset_subset_carrier by auto
            ultimately have "G.sumset {x'} (G.sumset A B) = G.sumset A B"
              by (metis G.finite_sumset G.sumset_subset_carrier card_subset_eq 
                G.card_sumset_singleton_subset_eq hA hB hx'G)
            then have "x'  ?K" using hx'G by (meson empty_subsetI G.finite_sumset hA hB insert_subset 
              G.sumset_eq_sub_stabilizer G.sumset_subset_carrier)
            then show "x  {K.Class [𝟬]}" using hxφ 
              by (metis K.Block_self K.Normal_def K.quotient.unit_closed insertCI)
          qed
        next
          show "{K.Class [𝟬]}  GK.stabilizer (K.Class ` G.sumset A B)"
            using GK.zero_mem_stabilizer by auto
        qed
        interpret group_epimorphism  G "([⊕])" "[𝟬]" "G.Factor_Group G ?K" 
          K.quotient_composition "K.Class [𝟬]" ..
        interpret GKN: normal_subgroup_in_kernel K.Class G "([⊕])" "[𝟬]" "G.Factor_Group G ?K" 
          K.quotient_composition "K.Class [𝟬]" ?K 
        proof
          show "?K  Ker" using K.Block_self K.Normal_def K.quotient.unit_closed by blast
        qed
        have hsumK: "card (G.sumset A B) = card ?K * card ( ` (G.sumset A B))"
          using G.finite_sumset hA hB G.sumset_subset_carrier G.Union_stabilizer_Class_eq 
          G.sumset_subset_carrier K.Union_Coset_card_eq by simp
        have hGKsumset: "GK.sumset ( ` A) ( ` B) =  ` (G.sumset A B)"
        proof
          show "GK.sumset ( ` A) ( ` B)    ` G.sumset A B"
          proof
            fix x assume "x  GK.sumset ( ` A) ( ` B)"
            then obtain a b where ha: "a  A" and hb: "b  B" and 
              "x = K.quotient_composition ( a) ( b)" using GK.sumset.cases by blast
            then have "x =  (a [⊕] b)" by (meson K.Class_commutes_with_composition hAG hBG in_mono)
            then show "x   ` G.sumset A B" using ha hb hAG hBG by blast
          qed
        next
          show "  ` G.sumset A B  GK.sumset ( ` A) ( ` B)"
          proof
            fix x assume "x   ` G.sumset A B"
            then obtain c where "c  G.sumset A B" and "x =  c" by blast
            then obtain a b where "a  A" and "b  B" and "x =  (a [⊕] b)" 
              using G.sumset.cases by metis
            then show "x  GK.sumset ( ` A) ( ` B)" using GK.sumset.cases 
              K.Class_commutes_with_composition hAG hBG in_mono
              by (smt (verit, best) GK.sumset.simps K.natural.map_closed imageI)  
          qed
        qed
        have hAK: "card (G.sumset A ?K) = card ?K * card ( ` A)" using hAG K.Union_Coset_card_eq hA
          G.sumset_stabilizer_eq_Class_Union G.Class_image_sumset_stabilizer_eq
          by (smt (verit, ccfv_threshold) card_0_eq G.card_sumset_0_iff G.finite_sumset hAne hB hBG hBne
            G.stabilizer_finite G.sumset_subset_carrier)
        have hBK: "card (G.sumset B ?K) = card ?K * card ( ` B)" using hBG K.Union_Coset_card_eq hB 
          G.sumset_stabilizer_eq_Class_Union  G.Class_image_sumset_stabilizer_eq
          by (smt (verit, ccfv_SIG) card_0_eq G.card_sumset_0_iff G.finite_sumset hA hAG hAne hBne 
            G.stabilizer_finite G.sumset_subset_carrier)
        have "card ( ` A)  card A" by (simp add: card_image_le hA)
        moreover have "card ( ` (G.sumset A B)) < card (G.sumset A B)" using hsumK hcardK_gt_1 
          G.card_sumset_0_iff hA hB hAne hBne by (metis card_eq_0_iff card_image_le hAG hBG 
          le_neq_implies_less less_not_refl3 mult_cancel2 nat_mult_1)
        ultimately have "card (GK.sumset ( ` A) ( ` B)) + card ( ` A) < card (G.sumset A B) + card A" 
          using hGKsumset by auto
        then obtain m where "m < n" and "card (GK.sumset ( ` A) ( ` B)) + card ( ` A) = m" 
          using hcardsum by blast
        moreover have hφAsub: " ` A  G.Factor_Group G ?K"
        proof
          fix x assume "x   ` A" then obtain a where "a  G" and " a = x" using hAG by blast
          then show "x  G.Factor_Group G ?K" by blast
        qed
        moreover have hφBsub: " ` B  G.Factor_Group G ?K"
        proof
          fix x assume "x   ` B" then obtain b where "b  G" and " b = x" using hBG by blast
          then show "x  G.Factor_Group G ?K" by blast
        qed
        moreover have hφA: "finite ( ` A)" and hφB: "finite ( ` B)" and hφAne: " ` A  {}" and 
          hφBne: " ` B  {}" using hA hB hAne hBne by auto
        moreover have "additive_abelian_group (G.Factor_Group G ?K) K.quotient_composition 
          (K.Class [𝟬])" ..
        moreover have "GK.stabilizer (GK.sumset ( ` A) ( ` B)) = {K.Class [𝟬]}" 
          using hstab0 hGKsumset by auto
        ultimately have hindφ: "card (GK.sumset ( ` A) ( ` B))   
          card (GK.sumset ( ` A) {K.Class [𝟬]}) + card (GK.sumset ( ` B) {K.Class [𝟬]}) - 1"
          using hindfactor[of "m" " ` A" " ` B"] by simp
        have hφsumA: "GK.sumset ( ` A) {K.Class [𝟬]} =  ` A"
          by (simp add: Int_absorb1 Int_commute hφAsub)
        have  hφsumB: "GK.sumset ( ` B) {K.Class [𝟬]} =  ` B"
          by (simp add: Int_absorb1 Int_commute hφBsub)
        have "card (G.sumset A ?K) + card (G.sumset B ?K) - card ?K = 
          card ?K * (card ( ` A) + card ( ` B) - 1)" 
          using hAK hBK add_mult_distrib2 diff_mult_distrib2 nat_mult_1_right by presburger
        also have "...  card ?K * card (GK.sumset ( ` A) ( ` B))" 
          using hindφ hφsumA hφsumB by simp
        finally show ?thesis by (simp add: hGKsumset hsumK)
      qed   
    qed
  qed
  thus ?thesis using assms hAne hBne additive_abelian_group_axioms by blast
qed

subsection‹Strict version of Kneser's Theorem›

text‹We show a strict version of Kneser's Theorem as presented in Theorem 3.2 of \cite{Ruzsa_book}.›

theorem Kneser_strict_aux:  fixes A and B assumes hAG: "A  G" and hBG: "B  G" and hA: "finite A" 
  and hB: "finite B" and hAne: "A  {}" and hBne: "B  {}" and 
  hineq: "card (sumset A B) >  card (sumset A (stabilizer (sumset A B))) + 
  card (sumset B (stabilizer (sumset A B))) - card (stabilizer (sumset A B))" 
  shows "card (sumset A B)  card A + card B"

proof-
  let ?H = "stabilizer (sumset A B)"
  have hfin: "finite ?H" using stabilizer_subset_group stabilizer_finite sumset_subset_carrier 
      finite_sumset assms sumset_is_empty_iff sumset_stabilizer_eq_self by metis
  have "card ?H dvd card (sumset A B)" and "card ?H dvd (card (sumset A (stabilizer (sumset A B))) + 
  card (sumset B (stabilizer (sumset A B))) - card ?H)" 
    using card_stabilizer_divide_sumset hAG hBG card_stabilizer_sumset_divide_sumset by auto
  then have "card (sumset A B)  card (sumset A ?H) + card (sumset B ?H)" using hineq
    by (metis diff_le_mono2 dvd_add_right_iff dvd_imp_le le_diff_conv less_imp_add_positive)
  moreover have "card A + card B  card (sumset A ?H) + card (sumset B ?H)" 
    using card_le_sumset sumset_commute assms stabilizer_subset_group stabilizer_is_nonempty 
      Int_emptyI inf.orderE add_mono hfin by metis
  ultimately show ?thesis by linarith
qed


theorem Kneser_strict:  fixes A and B assumes "A  G" and "B G" and "finite A" and "finite B"
  and "stabilizer (sumset A B) = H" and "A  {}" and "B  {}" and " card (sumset A B) < card A + card B"
  shows "card (sumset A B) = card (sumset A (stabilizer (sumset A B))) + 
    card (sumset B (stabilizer (sumset A B))) - card (stabilizer (sumset A B))"
  using Kneser Kneser_strict_aux assms le_antisym nat_less_le by metis

subsection‹The Cauchy–Davenport Theorem›

text‹We show the Cauchy–Davenport Theorem as a corollary of Kneser's Theorem, following a comment on
 Theorem 3.2 in \cite{Ruzsa_book}.›


interpretation Z_p: additive_abelian_group "{0..int ((p :: nat)-1)}" "(λ x y. ((x + y) mod int p))" "0::int"
  using additive_abelian_group_def residue_group[of "p"] by fastforce

theorem Cauchy_Davenport:
  fixes p :: nat
  assumes "prime p" and "A  {}" and "B  {}" and "finite A" and "finite B" and 
    "A  {0..p-1}" and "B  {0..p-1}"
  shows "card (Z_p.sumset p A B)  Min {p, card A + card B -1}" 

proof(cases "Z_p.stabilizer p (Z_p.sumset p A B) = {0}")
  case True
  moreover have "Z_p.sumset p A {0} = A" and "Z_p.sumset p B {0} = B" using assms Z_p.sumset_D(1) by auto
  ultimately show ?thesis using Z_p.Kneser[of "A" "p" "B"] assms by fastforce
next
  case hne: False
  let ?H = "Z_p.stabilizer p (Z_p.sumset p A B)"
  have "?H = {0..int(p-1)}" using hne Z_p.stabilizer_is_subgroup[of "p" "Z_p.sumset p A B"] 
    residue_group_simple[OF assms(1)] by blast
  moreover have "p  2" using assms(1) by (simp add: prime_ge_2_nat)
  ultimately have "card ?H = p" using card_atLeastAtMost by (simp add: of_nat_diff)
  then have "p  card (Z_p.sumset p A B)" 
    using Z_p.card_stabilizer_le card_0_eq assms Z_p.card_sumset_0_iff Z_p.sumset.cases 
      Z_p.sumset_subset_carrier Z_p.finite_sumset by metis
  then show ?thesis by auto 
qed


end
end