Taneb/Lagrange.agda

## Lagrange.agda
-- built on top of https://github.com/Taneb/agda-stdlib/commit/019b683a226a9eda942186aeab4b8d6be325e69c

{-# OPTIONS --without-K --safe #-}

module Lagrange where

open import Algebra.Bundles
open import Algebra.Core
open import Algebra.Morphism.Structures
open import Algebra.Properties.Group
open import Algebra.Structures
open import Data.Bool.Base
open import Data.Fin.Base hiding (_+_)
open import Data.Fin.Subset
open import Data.Fin.Subset.Induction
open import Data.Fin.Subset.Properties
import Data.Fin.Properties as Fin
open import Data.Nat.Base hiding (_⊔_)
open import Data.Nat.Divisibility
import Data.Nat.Properties as ℕ
open import Data.Product.Base as Σ
open import Data.Sum.Base
open import Data.Vec.Base hiding (group)
import Data.Vec.Properties as Vec
open import Function.Base
open import Function.Bundles hiding (_⇔_)
open import Induction.WellFounded
open import Level hiding (zero) renaming (suc to lsuc)
open import Relation.Binary.Bundles
open import Relation.Binary.Core hiding (_⇔_)
import Relation.Binary.Construct.On as On
open import Relation.Binary.Definitions hiding (Total; Empty)
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
open import Relation.Binary.Structures
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable
open import Relation.Nullary.Negation.Core

-- Finite setoids
------------------------------------------------------------------------

record HasOrder {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) (n : ℕ) : Set (a ⊔ ℓ) where
  field
    ι : Fin n → A
    injective : ∀ {i j} → ι i ≈ ι j → i ≡ j
    surjective : ∀ x → ∃[ i ] ι i ≈ x

order-cong : ∀ {a ℓ} {A : Set a} {_≈_ : Rel A ℓ} → IsEquivalence _≈_ → ∀ {m n} → HasOrder _≈_ m → HasOrder _≈_ n → m ≡ n
order-cong _ {m = zero} {n = zero} p q = refl
order-cong _ {m = zero} {n = suc n} p q = case proj₁ (p.surjective (q.ι zero)) of λ ()
  where
    module p = HasOrder p
    module q = HasOrder q
order-cong _ {m = suc m} {n = zero} p q = case proj₁ (q.surjective (p.ι zero)) of λ ()
  where
    module p = HasOrder p
    module q = HasOrder q
order-cong {_≈_ = _≈_} isEquivalence {m = suc m} {n = suc n} p q = cong suc (order-cong (On.isEquivalence proj₁ isEquivalence) p′ q′)
  where
    module ≈ = IsEquivalence isEquivalence
    module p = HasOrder p
    module q = HasOrder q
    A′ : Set _
    A′ = ∃[ x ] ¬ p.ι zero ≈ x
    _≈′_ : Rel A′ _
    _≈′_ = _≈_ on proj₁
    p′ : HasOrder _≈′_ m
    p′ = record
      { ι = λ i → p.ι (suc i) , λ eq → case p.injective eq of λ ()
      ; injective = λ eq → Fin.suc-injective (p.injective eq)
      ; surjective = λ (x , neq) → case p.surjective x of λ
        { (zero , eq) → contradiction eq neq
        ; (suc i , eq) → i , eq
        }
      }
    r : ∃[ r ] (q.ι r ≈ p.ι zero)
    r = q.surjective (p.ι zero)
    q′ : HasOrder _≈′_ n
    q′ = record
      { ι = λ i → q.ι (punchIn (proj₁ r) i) , λ eq → contradiction (sym (q.injective (≈.trans (proj₂ r) eq))) (Fin.punchInᵢ≢i (proj₁ r) i)
      ; injective = λ eq → Fin.punchIn-injective _ _ _ (q.injective eq)
      ; surjective = λ (x , neq) → case q.surjective x of λ
        { (i , eq) → punchOut (λ eq′ → contradiction (≈.trans (≈.sym (proj₂ r)) (≈.trans (≈.reflexive (cong q.ι eq′)) eq)) neq)
                   , ≈.trans (≈.reflexive (cong q.ι (Fin.punchIn-punchOut _))) eq
        }
      }

-- relation to Subset.∣_∣

order-∣-∣ : ∀ {a ℓ} {A : Setoid a ℓ} {m n} {p : Subset m} → HasOrder (Setoid._≈_ A) n → Bijection (On.setoid {B = ∃[ x ] x ∈ p } (setoid (Fin m)) proj₁) A → ∣ p ∣ ≡ n
order-∣-∣ {A = A} {n = zero} {p = []} order f = refl
order-∣-∣ {A = A} {n = suc n} {p = []} order f
  with () ← proj₁ (proj₁ (Bijection.surjective f (HasOrder.ι order zero)))
order-∣-∣ {A = A} {n = zero} {p = outside ∷ p} order f = order-∣-∣ {A = A} {p = p} order record
  { to = λ (x , x∈p) → f.to (suc x , there x∈p)
  ; cong = λ p → f.cong (cong suc p)
  ; bijective = record
    { fst = λ { {(x , x∈p)} {(y , y∈p)} f[x]≈f[y] → Fin.suc-injective (f.injective f[x]≈f[y]) }
    ; snd = λ y → case f.surjective y of λ
      { ((suc x , there x∈p) , eq) → (x , x∈p) , λ {refl → eq refl}
      }
    }
  }
  where module f = Bijection f
order-∣-∣ {A = A} {n = zero} {p = inside ∷ p} order f with () ← proj₁ (HasOrder.surjective order (Bijection.to f (zero , here)))
order-∣-∣ {A = A} {n = suc n} {p = outside ∷ p} order f = order-∣-∣ {A = A} {p = p} order record
  { to = λ (x , x∈p) → f.to (suc x , there x∈p)
  ; cong = λ p → f.cong (cong suc p)
  ; bijective = record
    { fst = λ { {(x , x∈p)} {(y , y∈p)} f[x]≈f[y] → Fin.suc-injective (f.injective f[x]≈f[y]) }
    ; snd = λ y → case f.surjective y of λ
      { ((suc x , there x∈p) , eq) → (x , x∈p) , λ {refl → eq refl}
      }
    }
  }
  where module f = Bijection f
order-∣-∣ {A = A} {n = suc n} {p = inside ∷ p} order f = cong suc $ order-∣-∣ {A = A′} {p = p} A′-hasOrder record
  { to = λ (x , x∈p) → record
    { fst = f.to (suc x , there x∈p)
    ; snd = λ eq → case f.injective eq of λ ()
    }
  ; cong = λ eq → f.cong (cong suc eq)
  ; bijective = record
    { fst = λ eq → Fin.suc-injective (f.injective eq)
    ; snd = λ {(y , prop) → case f.surjective y of λ
      { ((zero , here) , eq) → contradiction (eq refl) prop
      ; ((suc x , there x∈p) , eq) → record
        { fst = x , x∈p
        ; snd = λ { refl → eq refl }
        }
      }}
    }
  }
  where
    module A = Setoid A
    module order = HasOrder order
    module f = Bijection f
    A′ : Setoid _ _
    A′ = record
      { Carrier = ∃[ x ] ¬ f.to (zero , here) A.≈ x
      ; _≈_ = A._≈_ on proj₁
      ; isEquivalence = On.isEquivalence proj₁ A.isEquivalence
      }
    module A′ = Setoid A′
    i : Fin (suc n)
    i = proj₁ (order.surjective (f.to (zero , here)))
    i-prop : order.ι (order.surjective (f.to (zero , here)) .proj₁) A.≈ f.to (zero , here)
    i-prop = proj₂ (order.surjective (f.to (zero , here)))
    A′-hasOrder : HasOrder A′._≈_ n
    A′-hasOrder = record
      { ι = λ j → order.ι (punchIn i j) , λ eq → Fin.punchInᵢ≢i i j (sym (order.injective (A.trans i-prop eq)))
      ; injective = λ {j} {k} eq → Fin.punchIn-injective i j k (order.injective eq)
      ; surjective = λ { (x , prop) → case order.surjective x of λ
        { (j , eq) →
          let
            i≢j : i ≢ j
            i≢j i≡j = prop ((A.trans (A.sym i-prop) (A.trans (A.reflexive (cong order.ι i≡j)) eq)))
          in record
          { fst = punchOut {i = i} {j = j} i≢j
          ; snd = begin
            order.ι (punchIn i (punchOut i≢j)) ≡⟨ cong order.ι (Fin.punchIn-punchOut i≢j) ⟩
            order.ι j                         ≈⟨ eq ⟩
            x                                 ∎
          }
        }
      } }
      where open SetoidReasoning A

-- Finite groups
------------------------------------------------------------------------

record IsGroupOfOrder {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) (n : ℕ) : Set (a ⊔ ℓ) where
  field
    isGroup : IsGroup _≈_ _∙_ ε _⁻¹
    hasOrder : HasOrder _≈_ n

  open IsGroup isGroup public
  open HasOrder hasOrder public

  order-nonzero : NonZero n
  order-nonzero = ≢-nonZero λ { refl → case proj₁ (surjective ε) of λ () }

record GroupOfOrder c ℓ (n : ℕ) : Set (lsuc (c ⊔ ℓ)) where
  infix  8 _⁻¹
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_ : Rel Carrier ℓ
    _∙_ : Op₂ Carrier
    ε : Carrier
    _⁻¹ : Op₁ Carrier
    isGroupOfOrder : IsGroupOfOrder _≈_ _∙_ ε _⁻¹ n

  open IsGroupOfOrder isGroupOfOrder public

  group : Group c ℓ
  group = record { isGroup = isGroup }

  open Group group public
    using (monoid; semigroup; magma; rawGroup; rawMonoid; rawMagma)

open GroupOfOrder using (Carrier; rawGroup)

-- Lagrange's theorem
------------------------------------------------------------------------

module Lagrange {c ℓ m c′ ℓ′ n}
  (G : GroupOfOrder c ℓ m)
  (H : GroupOfOrder c′ ℓ′ n)
  (ι : Carrier G → Carrier H)
  (isGroupMonomorphism : IsGroupMonomorphism (rawGroup G) (rawGroup H) ι)
  where

  private
    module G = GroupOfOrder G
    module H = GroupOfOrder H
    module ι = IsGroupMonomorphism isGroupMonomorphism

  _∈G : Carrier H → Set (c ⊔ ℓ′)
  x ∈G = ∃[ g ] x H.≈ ι g

  _∈?G : ∀ x → Dec (x ∈G)
  x ∈?G with Fin.any? (λ i → proj₁ (H.surjective x) Fin.≟ proj₁ (H.surjective (ι (G.ι i))))
  ... | yes (i , eq) = yes (G.ι i , prf)
    where
      open SetoidReasoning H.setoid
      prf : x H.≈ ι (G.ι i)
      prf = begin
        x                                      ≈⟨ proj₂ (H.surjective x) ⟨
        H.ι (proj₁ (H.surjective x))           ≡⟨ cong H.ι eq ⟩
        H.ι (proj₁ (H.surjective (ι (G.ι i)))) ≈⟨ proj₂ (H.surjective (ι (G.ι i))) ⟩
        ι (G.ι i)                              ∎
  ... | no ¬p = no λ (g , eq) → contradiction (proj₁ (G.surjective g) , lemma g eq) ¬p
    where
      open SetoidReasoning H.setoid
      lemma : ∀ g → x H.≈ ι g → proj₁ (H.surjective x) ≡ proj₁ (H.surjective (ι (G.ι (proj₁ (G.surjective g)))))
      lemma g eq = H.injective $ begin
        H.ι (proj₁ (H.surjective x)) ≈⟨ proj₂ (H.surjective x) ⟩
        x ≈⟨ eq ⟩
        ι g ≈⟨ ι.⟦⟧-cong (proj₂ (G.surjective g)) ⟨
        ι (G.ι (proj₁ (G.surjective g))) ≈⟨ proj₂ (H.surjective (ι (G.ι (proj₁ (G.surjective g))))) ⟨
        H.ι (proj₁ (H.surjective (ι (G.ι (proj₁ (G.surjective g)))))) ∎


  _⇔_ : Rel (Carrier H) (c ⊔ ℓ′)
  x ⇔ y = ∃[ g ] x H.∙ ι g H.≈ y

  ≈⇒⇔ : ∀ {x y} → x H.≈ y → x ⇔ y
  ≈⇒⇔ x≈y = G.ε , H.trans (H.∙-congˡ ι.ε-homo) (H.trans (H.identityʳ _) x≈y)

  ⇔-refl : Reflexive _⇔_
  ⇔-refl {x} = G.ε , H.trans (H.∙-congˡ ι.ε-homo) (H.identityʳ x)

  ⇔-sym : Symmetric _⇔_
  ⇔-sym {x} {y} (g , eq) .proj₁ = g G.⁻¹
  ⇔-sym {x} {y} (g , eq) .proj₂ = begin
    y H.∙ ι (g G.⁻¹)         ≈⟨ H.∙-cong (H.sym eq) (ι.⁻¹-homo g) ⟩
    (x H.∙ ι g) H.∙ ι g H.⁻¹ ≈⟨ H.assoc x (ι g) (ι g H.⁻¹) ⟩
    x H.∙ (ι g H.∙ ι g H.⁻¹) ≈⟨ H.∙-congˡ (H.inverseʳ (ι g)) ⟩
    x H.∙ H.ε                ≈⟨ H.identityʳ x ⟩
    x                        ∎
    where open SetoidReasoning H.setoid

  ⇔-trans : Transitive _⇔_
  ⇔-trans (g₁ , eq₁) (g₂ , eq₂) .proj₁ = g₁ G.∙ g₂
  ⇔-trans {x} {y} {z} (g₁ , eq₁) (g₂ , eq₂) .proj₂ = begin
    x H.∙ ι (g₁ G.∙ g₂)   ≈⟨ H.∙-congˡ (ι.∙-homo g₁ g₂) ⟩
    x H.∙ (ι g₁ H.∙ ι g₂) ≈⟨ H.assoc x (ι g₁) (ι g₂) ⟨
    (x H.∙ ι g₁) H.∙ ι g₂ ≈⟨ H.∙-congʳ eq₁ ⟩
    y H.∙ ι g₂            ≈⟨ eq₂ ⟩
    z                     ∎
    where open SetoidReasoning H.setoid

  Coset : Carrier H → Set (c ⊔ c′ ⊔ ℓ′)
  Coset x = ∃[ y ] x ⇔ y

  [_]_≃_ : ∀ x → Rel (Coset x) ℓ′
  [_]_≃_ x = H._≈_ on proj₁

  [_]-setoid : Carrier H → Setoid (c ⊔ c′ ⊔ ℓ′) ℓ′
  [ x ]-setoid = record
    { _≈_ = [ x ]_≃_
    ; isEquivalence = On.isEquivalence proj₁ H.isEquivalence
    }

  ≃-hasOrder : ∀ x → HasOrder [ x ]_≃_ m
  ≃-hasOrder x = record
    { ι = λ i → x H.∙ ι (G.ι i) , G.ι i , H.refl
    ; injective = λ eq → G.injective (ι.injective (∙-cancelˡ H.group x _ _ eq))
    ; surjective = λ (y , g , eq) → case G.surjective g of λ
      { (i , eq′) → i , H.trans (H.∙-congˡ (ι.⟦⟧-cong eq′)) eq
      }
    }

  theorem : m ∣ n
  theorem = helper ⊤ ⊥
    (λ i → x∈p∪q⁺ (inj₂ ∈⊤))
    (λ (i , i∈⊥∩⊤) → ∉⊥ (proj₁ (x∈p∩q⁻ ⊥ ⊤ i∈⊥∩⊤)))
    (∣-trans (m ∣0) (∣-reflexive (sym (∣⊥∣≡0 n))))
    (λ _ i∈⊥ → contradiction i∈⊥ ∉⊥)
    where
      Helper : Subset n → Set (c ⊔ ℓ′)
      Helper r = (d : Subset n) → Total (d ∪ r) → Empty (d ∩ r) → m ∣ ∣ d ∣ → (∀ {i j} → H.ι i ⇔ H.ι j → i ∈ d → j ∈ d) → m ∣ n

      helper′ : ∀ r → WfRec _⊂_ Helper r → Helper r
      helper′ r rec d d∪r≡⊤ d∩r≡⊥ m∣∣d∣ d-has-cosets with nonempty? r
      ... | no empty = ∣-trans m∣∣d∣ $ ∣-reflexive $ begin
        ∣ d ∣     ≡⟨ cong ∣_∣ (∪-identityʳ d) ⟨
        ∣ d ∪ ⊥ ∣ ≡⟨ cong (λ r′ → ∣ d ∪ r′ ∣) (Empty-unique empty) ⟨
        ∣ d ∪ r ∣ ≡⟨ cong ∣_∣ (Total-unique d∪r≡⊤) ⟩
        ∣ ⊤ {n} ∣ ≡⟨ ∣⊤∣≡n n ⟩
        n         ∎
        where open ≡-Reasoning
      ... | yes (i , i∈r) = rec {r ─ coset} nextSubset (d ∪ coset) nextTotal nextEmpty nextMultiple nextCong
        where
          foo : ∀ {x} → x ∉ r → x ∈ d
          foo {x} x∉r with x∈p∪q⁻ d r (d∪r≡⊤ x)
          ... | inj₁ x∈d = x∈d
          ... | inj₂ x∈r = contradiction x∈r x∉r
          bar : ∀ {x} → x ∈ d → x ∉ r
          bar {x} x∈d x∈r = d∩r≡⊥ (x , x∈p∩q⁺ (x∈d , x∈r))

          r-has-cosets : ∀ {i j} → H.ι i ⇔ H.ι j → i ∈ r → j ∈ r
          r-has-cosets {i} {j} i⇔j i∈r = decidable-stable (j ∈? r) λ j∉r → contradiction i∈r (bar (d-has-cosets (⇔-sym i⇔j) (foo j∉r)))
          x : Carrier H
          x = H.ι i
          coset : Subset n
          coset = tabulate λ j → does ((x H.⁻¹ H.∙ H.ι j) ∈?G)
          i∈coset : i ∈ coset
          i∈coset = Vec.lookup⇒[]= i coset (trans
            (Vec.lookup∘tabulate (λ j → does ((x H.⁻¹ H.∙ H.ι j) ∈?G)) i)
            (dec-true ((x H.⁻¹ H.∙ H.ι i) ∈?G) (G.ε , H.trans (H.inverseˡ x) (H.sym ι.ε-homo))))

          coset-congˡ : ∀ {j} → x ⇔ H.ι j → j ∈ coset
          coset-congˡ {j} (g , x∙g≈j) = Vec.lookup⇒[]= j coset (trans (Vec.lookup∘tabulate _ j) (dec-true (_ ∈?G) x⁻¹∙j∈G))
            where
              open SetoidReasoning H.setoid
              x⁻¹∙j∈G : (x H.⁻¹ H.∙ H.ι j) ∈G
              x⁻¹∙j∈G .proj₁ = g
              x⁻¹∙j∈G .proj₂ = begin
                x H.⁻¹ H.∙ H.ι j ≈⟨ H.∙-congˡ x∙g≈j ⟨
                x H.⁻¹ H.∙ (x H.∙ ι g) ≈⟨ H.assoc (x H.⁻¹) x (ι g) ⟨
                (x H.⁻¹ H.∙ x) H.∙ ι g ≈⟨ H.∙-congʳ (H.inverseˡ x) ⟩
                H.ε H.∙ ι g ≈⟨ H.identityˡ (ι g) ⟩
                ι g ∎

          coset-congʳ : ∀ {j} → j ∈ coset → x ⇔ H.ι j
          coset-congʳ {j} j∈coset = record
            { fst = proj₁ x⁻¹∙j∈G
            ; snd = begin
              x H.∙ ι (proj₁ x⁻¹∙j∈G)  ≈⟨ H.∙-congˡ (proj₂ x⁻¹∙j∈G) ⟨
              x H.∙ (x H.⁻¹ H.∙ H.ι j) ≈⟨ H.assoc x (x H.⁻¹) (H.ι j) ⟨
              (x H.∙ x H.⁻¹) H.∙ H.ι j ≈⟨ H.∙-congʳ (H.inverseʳ x) ⟩
              H.ε H.∙ H.ι j            ≈⟨ H.identityˡ (H.ι j) ⟩
              H.ι j                    ∎
            }
            where
              open SetoidReasoning H.setoid
              p : does ((x H.⁻¹ H.∙ H.ι j) ∈?G) ≡ true
              p = trans (sym (Vec.lookup∘tabulate (λ k → does ((x H.⁻¹ H.∙ H.ι k) ∈?G)) j)) (Vec.[]=⇒lookup j∈coset)
              x⁻¹∙j∈G : (x H.⁻¹ H.∙ H.ι j) ∈G
              -- there must be a better way to do this
              x⁻¹∙j∈G = toWitness (subst T (sym (trans (isYes≗does (_ ∈?G)) p)) _)

          coset-cong : ∀ {j k} → H.ι j ⇔ H.ι k → j ∈ coset → k ∈ coset
          coset-cong j⇔k j∈coset = coset-congˡ (⇔-trans (coset-congʳ j∈coset) j⇔k)

          nextSubset : r ─ coset ⊂ r
          nextSubset = p─q⊆p r coset , i , i∈r , x∈p⇒x∉q─p i∈coset
          nextTotal : Total ((d ∪ coset) ∪ (r ─ coset))
          nextTotal j with j ∈? d
          ... | yes j∈d = x∈p∪q⁺ (inj₁ (x∈p∪q⁺ (inj₁ j∈d)))
          ... | no j∉d with j ∈? coset
          ... | yes j∈coset = x∈p∪q⁺ (inj₁ (x∈p∪q⁺ (inj₂ j∈coset)))
          ... | no j∉coset = x∈p∪q⁺ (inj₂ (x∈p∧x∉q⇒x∈p─q j∈r j∉coset))
            where
              j∈r : j ∈ r
              j∈r with x∈p∪q⁻ d r (d∪r≡⊤ j)
              ... | inj₁ j∈d = contradiction j∈d j∉d
              ... | inj₂ j∈r = j∈r
          nextEmpty : Empty ((d ∪ coset) ∩ (r ─ coset))
          nextEmpty (j , j∈[d∪coset]∩[r─coset])
            with (j∈d∪coset , j∈r─coset) ← x∈p∩q⁻ (d ∪ coset) (r ─ coset) j∈[d∪coset]∩[r─coset]
            with (j∈r , j∉coset) ← x∈p─q⁻ r coset j∈r─coset
            with x∈p∪q⁻ d coset j∈d∪coset
          ... | inj₁ j∈d = d∩r≡⊥ (j , x∈p∩q⁺ (j∈d , j∈r))
          ... | inj₂ j∈coset = j∉coset j∈coset

          j∈coset⇔Coset : Bijection (On.setoid {B = ∃[ j ] j ∈ coset} (setoid (Fin n)) proj₁) [ x ]-setoid
          j∈coset⇔Coset = record
            { to = λ (j , j∈coset) → record
              { fst = H.ι j
              ; snd = coset-congʳ j∈coset
              }
            ; cong = λ eq → H.reflexive (cong H.ι eq)
            ; bijective = record
              { fst = H.injective
              ; snd = λ
                { (y , x⇔y) → record
                  { fst = record
                    { fst = proj₁ (H.surjective y)
                    ; snd = coset-congˡ (⇔-trans x⇔y (⇔-sym (≈⇒⇔ (proj₂ (H.surjective y)))))
                    }
                  ; snd = λ
                    { refl → proj₂ (H.surjective y)
                    }
                  }
                }
              }
            }

          ∣coset∣≡m : ∣ coset ∣ ≡ m
          ∣coset∣≡m = order-∣-∣ (≃-hasOrder x) j∈coset⇔Coset

          coset⊆r : coset ⊆ r
          coset⊆r {j} j∈coset = r-has-cosets (coset-congʳ j∈coset) i∈r

          d∩coset-empty : Empty (d ∩ coset)
          d∩coset-empty (j , j∈d∩coset) with j∈d , j∈coset ← x∈p∩q⁻ d coset j∈d∩coset = d∩r≡⊥ (j , x∈p∩q⁺ (j∈d , coset⊆r j∈coset))

          nextMultiple′ : ∣ d ∣ + m ≡ ∣ d ∪ coset ∣
          nextMultiple′ = begin
            ∣ d ∣ + m                         ≡⟨⟩
            ∣ d ∣ + m ∸ 0                     ≡⟨ cong₂ _∸_ (cong (∣ d ∣ +_) ∣coset∣≡m) (trans (cong ∣_∣ (Empty-unique d∩coset-empty)) (∣⊥∣≡0 n)) ⟨
            ∣ d ∣ + ∣ coset ∣ ∸ ∣ d ∩ coset ∣ ≡⟨ counting d coset ⟨
            ∣ d ∪ coset ∣                     ∎
            where
              open ≡-Reasoning

          nextMultiple : m ∣ ∣ d ∪ coset ∣
          nextMultiple = begin
            m ∣⟨ ∣m∣n⇒∣m+n m∣∣d∣ n∣n ⟩
            ∣ d ∣ + m ≡⟨ nextMultiple′ ⟩
            ∣ d ∪ coset ∣ ∎
            where open ∣-Reasoning

          nextCong : ∀ {i j} → H.ι i ⇔ H.ι j → i ∈ d ∪ coset → j ∈ d ∪ coset
          nextCong i⇔j i∈d∪coset with x∈p∪q⁻ d coset i∈d∪coset
          ... | inj₁ i∈d = x∈p∪q⁺ (inj₁ (d-has-cosets i⇔j i∈d))
          ... | inj₂ i∈coset = x∈p∪q⁺ (inj₂ (coset-cong i⇔j i∈coset))

      helper : ∀ r → Helper r
      helper = All.wfRec ⊂-wellFounded (c ⊔ ℓ′) Helper helper′
	-- built on top of https://github.com/Taneb/agda-stdlib/commit/019b683a226a9eda942186aeab4b8d6be325e69c

	{-# OPTIONS --without-K --safe #-}

	module Lagrange where

	open import Algebra.Bundles
	open import Algebra.Core
	open import Algebra.Morphism.Structures
	open import Algebra.Properties.Group
	open import Algebra.Structures
	open import Data.Bool.Base
	open import Data.Fin.Base hiding (_+_)
	open import Data.Fin.Subset
	open import Data.Fin.Subset.Induction
	open import Data.Fin.Subset.Properties
	import Data.Fin.Properties as Fin
	open import Data.Nat.Base hiding (_⊔_)
	open import Data.Nat.Divisibility
	import Data.Nat.Properties as ℕ
	open import Data.Product.Base as Σ
	open import Data.Sum.Base
	open import Data.Vec.Base hiding (group)
	import Data.Vec.Properties as Vec
	open import Function.Base
	open import Function.Bundles hiding (_⇔_)
	open import Induction.WellFounded
	open import Level hiding (zero) renaming (suc to lsuc)
	open import Relation.Binary.Bundles
	open import Relation.Binary.Core hiding (_⇔_)
	import Relation.Binary.Construct.On as On
	open import Relation.Binary.Definitions hiding (Total; Empty)
	import Relation.Binary.Reasoning.Setoid as SetoidReasoning
	open import Relation.Binary.Structures
	open import Relation.Binary.PropositionalEquality
	open import Relation.Nullary.Decidable
	open import Relation.Nullary.Negation.Core

	-- Finite setoids
	------------------------------------------------------------------------

	record HasOrder {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) (n : ℕ) : Set (a ⊔ ℓ) where
	field
	ι : Fin n → A
	injective : ∀ {i j} → ι i ≈ ι j → i ≡ j
	surjective : ∀ x → ∃[ i ] ι i ≈ x

	order-cong : ∀ {a ℓ} {A : Set a} {_≈_ : Rel A ℓ} → IsEquivalence _≈_ → ∀ {m n} → HasOrder _≈_ m → HasOrder _≈_ n → m ≡ n
	order-cong _ {m = zero} {n = zero} p q = refl
	order-cong _ {m = zero} {n = suc n} p q = case proj₁ (p.surjective (q.ι zero)) of λ ()
	where
	module p = HasOrder p
	module q = HasOrder q
	order-cong _ {m = suc m} {n = zero} p q = case proj₁ (q.surjective (p.ι zero)) of λ ()
	where
	module p = HasOrder p
	module q = HasOrder q
	order-cong {_≈_ = _≈_} isEquivalence {m = suc m} {n = suc n} p q = cong suc (order-cong (On.isEquivalence proj₁ isEquivalence) p′ q′)
	where
	module ≈ = IsEquivalence isEquivalence
	module p = HasOrder p
	module q = HasOrder q
	A′ : Set _
	A′ = ∃[ x ] ¬ p.ι zero ≈ x
	_≈′_ : Rel A′ _
	_≈′_ = _≈_ on proj₁
	p′ : HasOrder _≈′_ m
	p′ = record
	{ ι = λ i → p.ι (suc i) , λ eq → case p.injective eq of λ ()
	; injective = λ eq → Fin.suc-injective (p.injective eq)
	; surjective = λ (x , neq) → case p.surjective x of λ
	{ (zero , eq) → contradiction eq neq
	; (suc i , eq) → i , eq
	}
	}
	r : ∃[ r ] (q.ι r ≈ p.ι zero)
	r = q.surjective (p.ι zero)
	q′ : HasOrder _≈′_ n
	q′ = record
	{ ι = λ i → q.ι (punchIn (proj₁ r) i) , λ eq → contradiction (sym (q.injective (≈.trans (proj₂ r) eq))) (Fin.punchInᵢ≢i (proj₁ r) i)
	; injective = λ eq → Fin.punchIn-injective _ _ _ (q.injective eq)
	; surjective = λ (x , neq) → case q.surjective x of λ
	{ (i , eq) → punchOut (λ eq′ → contradiction (≈.trans (≈.sym (proj₂ r)) (≈.trans (≈.reflexive (cong q.ι eq′)) eq)) neq)
	, ≈.trans (≈.reflexive (cong q.ι (Fin.punchIn-punchOut _))) eq
	}
	}

	-- relation to Subset.∣_∣

	order-∣-∣ : ∀ {a ℓ} {A : Setoid a ℓ} {m n} {p : Subset m} → HasOrder (Setoid._≈_ A) n → Bijection (On.setoid {B = ∃[ x ] x ∈ p } (setoid (Fin m)) proj₁) A → ∣ p ∣ ≡ n
	order-∣-∣ {A = A} {n = zero} {p = []} order f = refl
	order-∣-∣ {A = A} {n = suc n} {p = []} order f
	with () ← proj₁ (proj₁ (Bijection.surjective f (HasOrder.ι order zero)))
	order-∣-∣ {A = A} {n = zero} {p = outside ∷ p} order f = order-∣-∣ {A = A} {p = p} order record
	{ to = λ (x , x∈p) → f.to (suc x , there x∈p)
	; cong = λ p → f.cong (cong suc p)
	; bijective = record
	{ fst = λ { {(x , x∈p)} {(y , y∈p)} f[x]≈f[y] → Fin.suc-injective (f.injective f[x]≈f[y]) }
	; snd = λ y → case f.surjective y of λ
	{ ((suc x , there x∈p) , eq) → (x , x∈p) , λ {refl → eq refl}
	}
	}
	}
	where module f = Bijection f
	order-∣-∣ {A = A} {n = zero} {p = inside ∷ p} order f with () ← proj₁ (HasOrder.surjective order (Bijection.to f (zero , here)))
	order-∣-∣ {A = A} {n = suc n} {p = outside ∷ p} order f = order-∣-∣ {A = A} {p = p} order record
	{ to = λ (x , x∈p) → f.to (suc x , there x∈p)
	; cong = λ p → f.cong (cong suc p)
	; bijective = record
	{ fst = λ { {(x , x∈p)} {(y , y∈p)} f[x]≈f[y] → Fin.suc-injective (f.injective f[x]≈f[y]) }
	; snd = λ y → case f.surjective y of λ
	{ ((suc x , there x∈p) , eq) → (x , x∈p) , λ {refl → eq refl}
	}
	}
	}
	where module f = Bijection f
	order-∣-∣ {A = A} {n = suc n} {p = inside ∷ p} order f = cong suc $ order-∣-∣ {A = A′} {p = p} A′-hasOrder record
	{ to = λ (x , x∈p) → record
	{ fst = f.to (suc x , there x∈p)
	; snd = λ eq → case f.injective eq of λ ()
	}
	; cong = λ eq → f.cong (cong suc eq)
	; bijective = record
	{ fst = λ eq → Fin.suc-injective (f.injective eq)
	; snd = λ {(y , prop) → case f.surjective y of λ
	{ ((zero , here) , eq) → contradiction (eq refl) prop
	; ((suc x , there x∈p) , eq) → record
	{ fst = x , x∈p
	; snd = λ { refl → eq refl }
	}
	}}
	}
	}
	where
	module A = Setoid A
	module order = HasOrder order
	module f = Bijection f
	A′ : Setoid _ _
	A′ = record
	{ Carrier = ∃[ x ] ¬ f.to (zero , here) A.≈ x
	; _≈_ = A._≈_ on proj₁
	; isEquivalence = On.isEquivalence proj₁ A.isEquivalence
	}
	module A′ = Setoid A′
	i : Fin (suc n)
	i = proj₁ (order.surjective (f.to (zero , here)))
	i-prop : order.ι (order.surjective (f.to (zero , here)) .proj₁) A.≈ f.to (zero , here)
	i-prop = proj₂ (order.surjective (f.to (zero , here)))
	A′-hasOrder : HasOrder A′._≈_ n
	A′-hasOrder = record
	{ ι = λ j → order.ι (punchIn i j) , λ eq → Fin.punchInᵢ≢i i j (sym (order.injective (A.trans i-prop eq)))
	; injective = λ {j} {k} eq → Fin.punchIn-injective i j k (order.injective eq)
	; surjective = λ { (x , prop) → case order.surjective x of λ
	{ (j , eq) →
	let
	i≢j : i ≢ j
	i≢j i≡j = prop ((A.trans (A.sym i-prop) (A.trans (A.reflexive (cong order.ι i≡j)) eq)))
	in record
	{ fst = punchOut {i = i} {j = j} i≢j
	; snd = begin
	order.ι (punchIn i (punchOut i≢j)) ≡⟨ cong order.ι (Fin.punchIn-punchOut i≢j) ⟩
	order.ι j ≈⟨ eq ⟩
	x ∎
	}
	}
	} }
	where open SetoidReasoning A

	-- Finite groups
	------------------------------------------------------------------------

	record IsGroupOfOrder {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) (n : ℕ) : Set (a ⊔ ℓ) where
	field
	isGroup : IsGroup _≈_ _∙_ ε _⁻¹
	hasOrder : HasOrder _≈_ n

	open IsGroup isGroup public
	open HasOrder hasOrder public

	order-nonzero : NonZero n
	order-nonzero = ≢-nonZero λ { refl → case proj₁ (surjective ε) of λ () }

	record GroupOfOrder c ℓ (n : ℕ) : Set (lsuc (c ⊔ ℓ)) where
	infix 8 _⁻¹
	infixl 7 _∙_
	infix 4 _≈_
	field
	Carrier : Set c
	_≈_ : Rel Carrier ℓ
	_∙_ : Op₂ Carrier
	ε : Carrier
	_⁻¹ : Op₁ Carrier
	isGroupOfOrder : IsGroupOfOrder _≈_ _∙_ ε _⁻¹ n

	open IsGroupOfOrder isGroupOfOrder public

	group : Group c ℓ
	group = record { isGroup = isGroup }

	open Group group public
	using (monoid; semigroup; magma; rawGroup; rawMonoid; rawMagma)

	open GroupOfOrder using (Carrier; rawGroup)

	-- Lagrange's theorem
	------------------------------------------------------------------------

	module Lagrange {c ℓ m c′ ℓ′ n}
	(G : GroupOfOrder c ℓ m)
	(H : GroupOfOrder c′ ℓ′ n)
	(ι : Carrier G → Carrier H)
	(isGroupMonomorphism : IsGroupMonomorphism (rawGroup G) (rawGroup H) ι)
	where

	private
	module G = GroupOfOrder G
	module H = GroupOfOrder H
	module ι = IsGroupMonomorphism isGroupMonomorphism

	_∈G : Carrier H → Set (c ⊔ ℓ′)
	x ∈G = ∃[ g ] x H.≈ ι g

	_∈?G : ∀ x → Dec (x ∈G)
	x ∈?G with Fin.any? (λ i → proj₁ (H.surjective x) Fin.≟ proj₁ (H.surjective (ι (G.ι i))))
	... \| yes (i , eq) = yes (G.ι i , prf)
	where
	open SetoidReasoning H.setoid
	prf : x H.≈ ι (G.ι i)
	prf = begin
	x ≈⟨ proj₂ (H.surjective x) ⟨
	H.ι (proj₁ (H.surjective x)) ≡⟨ cong H.ι eq ⟩
	H.ι (proj₁ (H.surjective (ι (G.ι i)))) ≈⟨ proj₂ (H.surjective (ι (G.ι i))) ⟩
	ι (G.ι i) ∎
	... \| no ¬p = no λ (g , eq) → contradiction (proj₁ (G.surjective g) , lemma g eq) ¬p
	where
	open SetoidReasoning H.setoid
	lemma : ∀ g → x H.≈ ι g → proj₁ (H.surjective x) ≡ proj₁ (H.surjective (ι (G.ι (proj₁ (G.surjective g)))))
	lemma g eq = H.injective $ begin
	H.ι (proj₁ (H.surjective x)) ≈⟨ proj₂ (H.surjective x) ⟩
	x ≈⟨ eq ⟩
	ι g ≈⟨ ι.⟦⟧-cong (proj₂ (G.surjective g)) ⟨
	ι (G.ι (proj₁ (G.surjective g))) ≈⟨ proj₂ (H.surjective (ι (G.ι (proj₁ (G.surjective g))))) ⟨
	H.ι (proj₁ (H.surjective (ι (G.ι (proj₁ (G.surjective g)))))) ∎


	_⇔_ : Rel (Carrier H) (c ⊔ ℓ′)
	x ⇔ y = ∃[ g ] x H.∙ ι g H.≈ y

	≈⇒⇔ : ∀ {x y} → x H.≈ y → x ⇔ y
	≈⇒⇔ x≈y = G.ε , H.trans (H.∙-congˡ ι.ε-homo) (H.trans (H.identityʳ _) x≈y)

	⇔-refl : Reflexive _⇔_
	⇔-refl {x} = G.ε , H.trans (H.∙-congˡ ι.ε-homo) (H.identityʳ x)

	⇔-sym : Symmetric _⇔_
	⇔-sym {x} {y} (g , eq) .proj₁ = g G.⁻¹
	⇔-sym {x} {y} (g , eq) .proj₂ = begin
	y H.∙ ι (g G.⁻¹) ≈⟨ H.∙-cong (H.sym eq) (ι.⁻¹-homo g) ⟩
	(x H.∙ ι g) H.∙ ι g H.⁻¹ ≈⟨ H.assoc x (ι g) (ι g H.⁻¹) ⟩
	x H.∙ (ι g H.∙ ι g H.⁻¹) ≈⟨ H.∙-congˡ (H.inverseʳ (ι g)) ⟩
	x H.∙ H.ε ≈⟨ H.identityʳ x ⟩
	x ∎
	where open SetoidReasoning H.setoid

	⇔-trans : Transitive _⇔_
	⇔-trans (g₁ , eq₁) (g₂ , eq₂) .proj₁ = g₁ G.∙ g₂
	⇔-trans {x} {y} {z} (g₁ , eq₁) (g₂ , eq₂) .proj₂ = begin
	x H.∙ ι (g₁ G.∙ g₂) ≈⟨ H.∙-congˡ (ι.∙-homo g₁ g₂) ⟩
	x H.∙ (ι g₁ H.∙ ι g₂) ≈⟨ H.assoc x (ι g₁) (ι g₂) ⟨
	(x H.∙ ι g₁) H.∙ ι g₂ ≈⟨ H.∙-congʳ eq₁ ⟩
	y H.∙ ι g₂ ≈⟨ eq₂ ⟩
	z ∎
	where open SetoidReasoning H.setoid

	Coset : Carrier H → Set (c ⊔ c′ ⊔ ℓ′)
	Coset x = ∃[ y ] x ⇔ y

	[_]_≃_ : ∀ x → Rel (Coset x) ℓ′
	[_]_≃_ x = H._≈_ on proj₁

	[_]-setoid : Carrier H → Setoid (c ⊔ c′ ⊔ ℓ′) ℓ′
	[ x ]-setoid = record
	{ _≈_ = [ x ]_≃_
	; isEquivalence = On.isEquivalence proj₁ H.isEquivalence
	}

	≃-hasOrder : ∀ x → HasOrder [ x ]_≃_ m
	≃-hasOrder x = record
	{ ι = λ i → x H.∙ ι (G.ι i) , G.ι i , H.refl
	; injective = λ eq → G.injective (ι.injective (∙-cancelˡ H.group x _ _ eq))
	; surjective = λ (y , g , eq) → case G.surjective g of λ
	{ (i , eq′) → i , H.trans (H.∙-congˡ (ι.⟦⟧-cong eq′)) eq
	}
	}

	theorem : m ∣ n
	theorem = helper ⊤ ⊥
	(λ i → x∈p∪q⁺ (inj₂ ∈⊤))
	(λ (i , i∈⊥∩⊤) → ∉⊥ (proj₁ (x∈p∩q⁻ ⊥ ⊤ i∈⊥∩⊤)))
	(∣-trans (m ∣0) (∣-reflexive (sym (∣⊥∣≡0 n))))
	(λ _ i∈⊥ → contradiction i∈⊥ ∉⊥)
	where
	Helper : Subset n → Set (c ⊔ ℓ′)
	Helper r = (d : Subset n) → Total (d ∪ r) → Empty (d ∩ r) → m ∣ ∣ d ∣ → (∀ {i j} → H.ι i ⇔ H.ι j → i ∈ d → j ∈ d) → m ∣ n

	helper′ : ∀ r → WfRec _⊂_ Helper r → Helper r
	helper′ r rec d d∪r≡⊤ d∩r≡⊥ m∣∣d∣ d-has-cosets with nonempty? r
	... \| no empty = ∣-trans m∣∣d∣ $ ∣-reflexive $ begin
	∣ d ∣ ≡⟨ cong ∣_∣ (∪-identityʳ d) ⟨
	∣ d ∪ ⊥ ∣ ≡⟨ cong (λ r′ → ∣ d ∪ r′ ∣) (Empty-unique empty) ⟨
	∣ d ∪ r ∣ ≡⟨ cong ∣_∣ (Total-unique d∪r≡⊤) ⟩
	∣ ⊤ {n} ∣ ≡⟨ ∣⊤∣≡n n ⟩
	n ∎
	where open ≡-Reasoning
	... \| yes (i , i∈r) = rec {r ─ coset} nextSubset (d ∪ coset) nextTotal nextEmpty nextMultiple nextCong
	where
	foo : ∀ {x} → x ∉ r → x ∈ d
	foo {x} x∉r with x∈p∪q⁻ d r (d∪r≡⊤ x)
	... \| inj₁ x∈d = x∈d
	... \| inj₂ x∈r = contradiction x∈r x∉r
	bar : ∀ {x} → x ∈ d → x ∉ r
	bar {x} x∈d x∈r = d∩r≡⊥ (x , x∈p∩q⁺ (x∈d , x∈r))

	r-has-cosets : ∀ {i j} → H.ι i ⇔ H.ι j → i ∈ r → j ∈ r
	r-has-cosets {i} {j} i⇔j i∈r = decidable-stable (j ∈? r) λ j∉r → contradiction i∈r (bar (d-has-cosets (⇔-sym i⇔j) (foo j∉r)))
	x : Carrier H
	x = H.ι i
	coset : Subset n
	coset = tabulate λ j → does ((x H.⁻¹ H.∙ H.ι j) ∈?G)
	i∈coset : i ∈ coset
	i∈coset = Vec.lookup⇒[]= i coset (trans
	(Vec.lookup∘tabulate (λ j → does ((x H.⁻¹ H.∙ H.ι j) ∈?G)) i)
	(dec-true ((x H.⁻¹ H.∙ H.ι i) ∈?G) (G.ε , H.trans (H.inverseˡ x) (H.sym ι.ε-homo))))

	coset-congˡ : ∀ {j} → x ⇔ H.ι j → j ∈ coset
	coset-congˡ {j} (g , x∙g≈j) = Vec.lookup⇒[]= j coset (trans (Vec.lookup∘tabulate _ j) (dec-true (_ ∈?G) x⁻¹∙j∈G))
	where
	open SetoidReasoning H.setoid
	x⁻¹∙j∈G : (x H.⁻¹ H.∙ H.ι j) ∈G
	x⁻¹∙j∈G .proj₁ = g
	x⁻¹∙j∈G .proj₂ = begin
	x H.⁻¹ H.∙ H.ι j ≈⟨ H.∙-congˡ x∙g≈j ⟨
	x H.⁻¹ H.∙ (x H.∙ ι g) ≈⟨ H.assoc (x H.⁻¹) x (ι g) ⟨
	(x H.⁻¹ H.∙ x) H.∙ ι g ≈⟨ H.∙-congʳ (H.inverseˡ x) ⟩
	H.ε H.∙ ι g ≈⟨ H.identityˡ (ι g) ⟩
	ι g ∎

	coset-congʳ : ∀ {j} → j ∈ coset → x ⇔ H.ι j
	coset-congʳ {j} j∈coset = record
	{ fst = proj₁ x⁻¹∙j∈G
	; snd = begin
	x H.∙ ι (proj₁ x⁻¹∙j∈G) ≈⟨ H.∙-congˡ (proj₂ x⁻¹∙j∈G) ⟨
	x H.∙ (x H.⁻¹ H.∙ H.ι j) ≈⟨ H.assoc x (x H.⁻¹) (H.ι j) ⟨
	(x H.∙ x H.⁻¹) H.∙ H.ι j ≈⟨ H.∙-congʳ (H.inverseʳ x) ⟩
	H.ε H.∙ H.ι j ≈⟨ H.identityˡ (H.ι j) ⟩
	H.ι j ∎
	}
	where
	open SetoidReasoning H.setoid
	p : does ((x H.⁻¹ H.∙ H.ι j) ∈?G) ≡ true
	p = trans (sym (Vec.lookup∘tabulate (λ k → does ((x H.⁻¹ H.∙ H.ι k) ∈?G)) j)) (Vec.[]=⇒lookup j∈coset)
	x⁻¹∙j∈G : (x H.⁻¹ H.∙ H.ι j) ∈G
	-- there must be a better way to do this
	x⁻¹∙j∈G = toWitness (subst T (sym (trans (isYes≗does (_ ∈?G)) p)) _)

	coset-cong : ∀ {j k} → H.ι j ⇔ H.ι k → j ∈ coset → k ∈ coset
	coset-cong j⇔k j∈coset = coset-congˡ (⇔-trans (coset-congʳ j∈coset) j⇔k)

	nextSubset : r ─ coset ⊂ r
	nextSubset = p─q⊆p r coset , i , i∈r , x∈p⇒x∉q─p i∈coset
	nextTotal : Total ((d ∪ coset) ∪ (r ─ coset))
	nextTotal j with j ∈? d
	... \| yes j∈d = x∈p∪q⁺ (inj₁ (x∈p∪q⁺ (inj₁ j∈d)))
	... \| no j∉d with j ∈? coset
	... \| yes j∈coset = x∈p∪q⁺ (inj₁ (x∈p∪q⁺ (inj₂ j∈coset)))
	... \| no j∉coset = x∈p∪q⁺ (inj₂ (x∈p∧x∉q⇒x∈p─q j∈r j∉coset))
	where
	j∈r : j ∈ r
	j∈r with x∈p∪q⁻ d r (d∪r≡⊤ j)
	... \| inj₁ j∈d = contradiction j∈d j∉d
	... \| inj₂ j∈r = j∈r
	nextEmpty : Empty ((d ∪ coset) ∩ (r ─ coset))
	nextEmpty (j , j∈[d∪coset]∩[r─coset])
	with (j∈d∪coset , j∈r─coset) ← x∈p∩q⁻ (d ∪ coset) (r ─ coset) j∈[d∪coset]∩[r─coset]
	with (j∈r , j∉coset) ← x∈p─q⁻ r coset j∈r─coset
	with x∈p∪q⁻ d coset j∈d∪coset
	... \| inj₁ j∈d = d∩r≡⊥ (j , x∈p∩q⁺ (j∈d , j∈r))
	... \| inj₂ j∈coset = j∉coset j∈coset

	j∈coset⇔Coset : Bijection (On.setoid {B = ∃[ j ] j ∈ coset} (setoid (Fin n)) proj₁) [ x ]-setoid
	j∈coset⇔Coset = record
	{ to = λ (j , j∈coset) → record
	{ fst = H.ι j
	; snd = coset-congʳ j∈coset
	}
	; cong = λ eq → H.reflexive (cong H.ι eq)
	; bijective = record
	{ fst = H.injective
	; snd = λ
	{ (y , x⇔y) → record
	{ fst = record
	{ fst = proj₁ (H.surjective y)
	; snd = coset-congˡ (⇔-trans x⇔y (⇔-sym (≈⇒⇔ (proj₂ (H.surjective y)))))
	}
	; snd = λ
	{ refl → proj₂ (H.surjective y)
	}
	}
	}
	}
	}

	∣coset∣≡m : ∣ coset ∣ ≡ m
	∣coset∣≡m = order-∣-∣ (≃-hasOrder x) j∈coset⇔Coset

	coset⊆r : coset ⊆ r
	coset⊆r {j} j∈coset = r-has-cosets (coset-congʳ j∈coset) i∈r

	d∩coset-empty : Empty (d ∩ coset)
	d∩coset-empty (j , j∈d∩coset) with j∈d , j∈coset ← x∈p∩q⁻ d coset j∈d∩coset = d∩r≡⊥ (j , x∈p∩q⁺ (j∈d , coset⊆r j∈coset))

	nextMultiple′ : ∣ d ∣ + m ≡ ∣ d ∪ coset ∣
	nextMultiple′ = begin
	∣ d ∣ + m ≡⟨⟩
	∣ d ∣ + m ∸ 0 ≡⟨ cong₂ _∸_ (cong (∣ d ∣ +_) ∣coset∣≡m) (trans (cong ∣_∣ (Empty-unique d∩coset-empty)) (∣⊥∣≡0 n)) ⟨
	∣ d ∣ + ∣ coset ∣ ∸ ∣ d ∩ coset ∣ ≡⟨ counting d coset ⟨
	∣ d ∪ coset ∣ ∎
	where
	open ≡-Reasoning

	nextMultiple : m ∣ ∣ d ∪ coset ∣
	nextMultiple = begin
	m ∣⟨ ∣m∣n⇒∣m+n m∣∣d∣ n∣n ⟩
	∣ d ∣ + m ≡⟨ nextMultiple′ ⟩
	∣ d ∪ coset ∣ ∎
	where open ∣-Reasoning

	nextCong : ∀ {i j} → H.ι i ⇔ H.ι j → i ∈ d ∪ coset → j ∈ d ∪ coset
	nextCong i⇔j i∈d∪coset with x∈p∪q⁻ d coset i∈d∪coset
	... \| inj₁ i∈d = x∈p∪q⁺ (inj₁ (d-has-cosets i⇔j i∈d))
	... \| inj₂ i∈coset = x∈p∪q⁺ (inj₂ (coset-cong i⇔j i∈coset))

	helper : ∀ r → Helper r
	helper = All.wfRec ⊂-wellFounded (c ⊔ ℓ′) Helper helper′
No results found