Physlib.StringTheory.FTheory.SU5.Fluxes.NoExotics.Elems

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.StringTheory.FTheory.SU5.Fluxes.Basic

Terms of `FluxesFive` and `FluxesTen` with no chiral exotics

i. Overview

In this module we give the terms of type FluxesFive and FluxesTen which obey the NoExotics and HasNoZero propositions.

In each case, there is only a finite set of such elements, which we give explicitly. We show that these sets are complete in the module StringTheory.FTheory.SU5.Fluxes.NoExotics.Completeness.

This module is reserved for the explicit sets of elements, and simple lemmas about the elements of those elements.

ii. Key results

FluxesFive.elemsNoExotics : The multiset of elements of FluxesFive which obey NoExotics and HasNoZero.

FluxesTen.elemsNoExotics : The multiset of elements of FluxesTen which obey NoExotics and HasNoZero.

iii. Table of contents

A. The multiset sets of FluxesFive with no chiral exotics and no zero fluxes

A.1. The definition of the multiset

A.2. The cardinality of the multiset is 31

A.3. The multiset has no duplicates

A.4. Every element of the multiset obeys NoExotics

A.5. Every element of the multiset has at most 4 distinct flux pairs

A.6. Every element of the multiset has at most 6 flux pairs

A.7. The sum of all flux-pairs in any element of the multiset is (3, 0)

A.8. Every element of the multiset obeys HasNoZero

A.9. A sum relation for subsets of elements of the multiset

B. The multiset sets of FluxesFive with no chiral exotics and no zero fluxes

B.1. The definition of the multiset

B.2. The cardinality of the multiset is 6

B.3. The multiset has no duplicates

B.4. Every element of the multiset obeys NoExotics

B.5. Every element of the multiset has at most 3 distinct flux pairs

B.6. The sum of all flux-pairs in any element of the multiset is (3, 0)

B.7. Every element of the multiset obeys HasNoZero

iv. References

There are no known references for the material in this module.

@[expose] public section

A. The multiset sets of `FluxesFive` with no chiral exotics and no zero fluxes

A.1. The definition of the multiset

The elements of FluxesFive for which the NoExotics condition holds.

def elemsNoExotics : Multiset FluxesFive := {
    {⟨1, -1⟩, ⟨1, -1⟩, ⟨1, -1⟩, ⟨0, 1⟩, ⟨0, 1⟩, ⟨0, 1⟩},
    {⟨1, -1⟩, ⟨1, -1⟩, ⟨1, -1⟩, ⟨0, 1⟩, ⟨0, 2⟩},
    {⟨1, -1⟩, ⟨1, -1⟩, ⟨1, 0⟩, ⟨0, 1⟩, ⟨0, 1⟩},
    {⟨1, 1⟩, ⟨1, -1⟩, ⟨1, -1⟩, ⟨0, 1⟩},
    {⟨1, 0⟩, ⟨1, 0⟩, ⟨1, -1⟩, ⟨0, 1⟩},
    {⟨1, -1⟩, ⟨1, 0⟩, ⟨1, -1⟩, ⟨0, 2⟩},
    {⟨1, -1⟩, ⟨1, -1⟩, ⟨1, -1⟩, ⟨0, 3⟩},
    {⟨1, -1⟩, ⟨1, -1⟩, ⟨1, 2⟩},
    {⟨1, -1⟩, ⟨1, 0⟩, ⟨1, 1⟩}, {⟨1, 0⟩, ⟨1, 0⟩, ⟨1, 0⟩},
    {⟨1, -1⟩, ⟨2, -2⟩, ⟨0, 1⟩, ⟨0, 1⟩, ⟨0, 1⟩},
    {⟨1, -1⟩, ⟨2, -2⟩, ⟨0, 1⟩, ⟨0, 2⟩},
    {⟨1, -1⟩, ⟨2, -1⟩, ⟨0, 1⟩, ⟨0, 1⟩},
    {⟨1, 0⟩, ⟨2, -2⟩, ⟨0, 1⟩, ⟨0, 1⟩},
    {⟨1, 1⟩, ⟨2, -2⟩, ⟨0, 1⟩}, {⟨1, 0⟩, ⟨2, -1⟩, ⟨0, 1⟩},
    {⟨1, 0⟩, ⟨2, -2⟩, ⟨0, 2⟩}, {⟨1, -1⟩, ⟨2, 0⟩, ⟨0, 1⟩},
    {⟨1, -1⟩, ⟨2, -1⟩, ⟨0, 2⟩}, {⟨1, -1⟩, ⟨2, -2⟩, ⟨0, 3⟩},
    {⟨1, -1⟩, ⟨2, 1⟩}, {⟨1, 0⟩, ⟨2, 0⟩}, {⟨1, 1⟩, ⟨2, -1⟩},
    {⟨1, 2⟩, ⟨2, -2⟩},
    {⟨3, -3⟩, ⟨0, 1⟩, ⟨0, 1⟩, ⟨0, 1⟩},
    {⟨3, -3⟩, ⟨0, 1⟩, ⟨0, 2⟩}, {⟨3, -2⟩, ⟨0, 1⟩, ⟨0, 1⟩},
    {⟨3, -3⟩, ⟨0, 3⟩}, {⟨3, -2⟩, ⟨0, 2⟩}, {⟨3, -1⟩, ⟨0, 1⟩},
    {⟨3, 0⟩}}

A.2. The cardinality of the multiset is 31

lemma elemsNoExotics_card : elemsNoExotics.card = 31 := by⊢ elemsNoExotics.card = 31
  decideAll goals completed! 🐙

A.3. The multiset has no duplicates

lemma elemsNoExotics_nodup : elemsNoExotics.Nodup := by⊢ elemsNoExotics.Nodup
  decideAll goals completed! 🐙

A.4. Every element of the multiset obeys `NoExotics`

lemma noExotics_of_mem_elemsNoExotics (F : FluxesFive) (h : F ∈ elemsNoExotics) :
    NoExotics F := byF:FluxesFiveh:F ∈ elemsNoExotics⊢ F.NoExotics
  revert F⊢ ∀ F ∈ elemsNoExotics, F.NoExotics
  decideAll goals completed! 🐙

A.5. Every element of the multiset has at most 4 distinct flux pairs

lemma toFinset_card_le_four_mem_elemsNoExotics (F : FluxesFive) (h : F ∈ elemsNoExotics) :
    F.toFinset.card ≤ 4 := byF:FluxesFiveh:F ∈ elemsNoExotics⊢ (Multiset.toFinset F).card ≤ 4
  revert F h⊢ ∀ F ∈ elemsNoExotics, (Multiset.toFinset F).card ≤ 4
  decideAll goals completed! 🐙

A.6. Every element of the multiset has at most 6 flux pairs

lemma card_le_six_mem_elemsNoExotics (F : FluxesFive) (h : F ∈ elemsNoExotics) :
    F.card ≤ 6 := byF:FluxesFiveh:F ∈ elemsNoExotics⊢ Multiset.card F ≤ 6
  revert F h⊢ ∀ F ∈ elemsNoExotics, Multiset.card F ≤ 6
  decideAll goals completed! 🐙

A.7. The sum of all flux-pairs in any element of the multiset is (3, 0)

lemma sum_of_mem_elemsNoExotics (F : FluxesFive) (h : F ∈ elemsNoExotics) :
    F.sum = ⟨3, 0⟩ := byF:FluxesFiveh:F ∈ elemsNoExotics⊢ Multiset.sum F = { M := 3, N := 0 }
  revert F h⊢ ∀ F ∈ elemsNoExotics, Multiset.sum F = { M := 3, N := 0 }
  decideAll goals completed! 🐙

A.8. Every element of the multiset obeys `HasNoZero`

lemma hasNoZero_of_mem_elemsNoExotics (F : FluxesFive) (h : F ∈ elemsNoExotics) :
    F.HasNoZero := byF:FluxesFiveh:F ∈ elemsNoExotics⊢ F.HasNoZero
  revert F h⊢ ∀ F ∈ elemsNoExotics, F.HasNoZero
  decideAll goals completed! 🐙

A.9. A sum relation for subsets of elements of the multiset

lemma map_sum_add_of_mem_powerset_elemsNoExotics (F S : FluxesFive)
    (hf : F ∈ FluxesFive.elemsNoExotics)
    (hS: S ∈ Multiset.powerset F) :
    (S.map (fun x => ⟨|x.1|, -|x.1|⟩)).sum +
    (S.map (fun x => ⟨(0 : ℤ), |x.1 + x.2|⟩)).sum = S.sum := byF:FluxesFiveS:FluxesFivehf:F ∈ elemsNoExoticshS:S ∈ Multiset.powerset F⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S
  fin_cases hf«0»S:FluxesFivehS:S ∈
  Multiset.powerset
    {{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 },
      { M := 0, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«1»S:FluxesFivehS:S ∈
  Multiset.powerset
    {{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 2 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«2»S:FluxesFivehS:S ∈
  Multiset.powerset
    {{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 1 }, { M := 0, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«3»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«4»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := 0 }, { M := 1, N := 0 }, { M := 1, N := -1 }, { M := 0, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«5»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 1, N := -1 }, { M := 0, N := 2 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«6»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 3 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«7»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := 2 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«8»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 1, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«9»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := 0 }, { M := 1, N := 0 }, { M := 1, N := 0 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«10»S:FluxesFivehS:S ∈
  Multiset.powerset
    {{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«11»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 2 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«12»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := -1 }, { M := 2, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«13»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := 0 }, { M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«14»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := 1 }, { M := 2, N := -2 }, { M := 0, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«15»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := 0 }, { M := 2, N := -1 }, { M := 0, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«16»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := 0 }, { M := 2, N := -2 }, { M := 0, N := 2 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«17»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := -1 }, { M := 2, N := 0 }, { M := 0, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«18»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := -1 }, { M := 2, N := -1 }, { M := 0, N := 2 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«19»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 3 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«20»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := -1 }, { M := 2, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«21»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := 0 }, { M := 2, N := 0 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«22»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := 1 }, { M := 2, N := -1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«23»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := 2 }, { M := 2, N := -2 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«24»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 3, N := -3 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«25»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 3, N := -3 }, { M := 0, N := 1 }, { M := 0, N := 2 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«26»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 3, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«27»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 3, N := -3 }, { M := 0, N := 3 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«28»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 3, N := -2 }, { M := 0, N := 2 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«29»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 3, N := -1 }, { M := 0, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«30»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 3, N := 0 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S <;>«0»S:FluxesFivehS:S ∈
  Multiset.powerset
    {{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 },
      { M := 0, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«1»S:FluxesFivehS:S ∈
  Multiset.powerset
    {{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 2 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«2»S:FluxesFivehS:S ∈
  Multiset.powerset
    {{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 1 }, { M := 0, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«3»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«4»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := 0 }, { M := 1, N := 0 }, { M := 1, N := -1 }, { M := 0, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«5»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 1, N := -1 }, { M := 0, N := 2 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«6»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 3 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«7»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := 2 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«8»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 1, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«9»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := 0 }, { M := 1, N := 0 }, { M := 1, N := 0 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«10»S:FluxesFivehS:S ∈
  Multiset.powerset
    {{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«11»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 2 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«12»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := -1 }, { M := 2, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«13»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := 0 }, { M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«14»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := 1 }, { M := 2, N := -2 }, { M := 0, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«15»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := 0 }, { M := 2, N := -1 }, { M := 0, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«16»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := 0 }, { M := 2, N := -2 }, { M := 0, N := 2 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«17»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := -1 }, { M := 2, N := 0 }, { M := 0, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«18»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := -1 }, { M := 2, N := -1 }, { M := 0, N := 2 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«19»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 3 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«20»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := -1 }, { M := 2, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«21»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := 0 }, { M := 2, N := 0 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«22»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := 1 }, { M := 2, N := -1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«23»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 1, N := 2 }, { M := 2, N := -2 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«24»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 3, N := -3 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«25»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 3, N := -3 }, { M := 0, N := 1 }, { M := 0, N := 2 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«26»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 3, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«27»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 3, N := -3 }, { M := 0, N := 3 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«28»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 3, N := -2 }, { M := 0, N := 2 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«29»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 3, N := -1 }, { M := 0, N := 1 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S«30»S:FluxesFivehS:S ∈ Multiset.powerset {{ M := 3, N := 0 }}⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) S).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) S).sum =
  Multiset.sum S fin_cases hS«30».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«30».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 3, N := 0 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 3, N := 0 }]).sum =
  (↑[{ M := 3, N := 0 }]).sum <;>«0».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«0».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }]).sum«0».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }]).sum«0».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum«0».«4»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }]).sum«0».«5»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum«0».«6»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum«0».«7»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }]).sum«0».«8»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }]).sum«0».«9»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum«0».«10»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum«0».«11»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum«0».«12»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum«0».«13»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum«0».«14»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum«0».«15»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum«0».«16»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }]).sum«0».«17»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum«0».«18»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum«0».«19»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum«0».«20»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum«0».«21»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum«0».«22»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum«0».«23»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum«0».«24»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«25»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«26»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«27»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«28»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«29»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«30»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«31»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«32»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }]).sum«0».«33»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum«0».«34»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum«0».«35»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum«0».«36»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum«0».«37»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum«0».«38»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum«0».«39»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum«0».«40»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«41»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«42»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«43»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«44»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«45»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«46»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«47»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«48»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«49»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«50»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«51»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«52»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«53»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«54»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«55»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«56»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«57»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«58»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«59»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«60»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«61»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«62»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«0».«63»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 },
            { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 },
            { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 },
        { M := 0, N := 1 }]).sum«1».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«1».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }]).sum«1».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }]).sum«1».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum«1».«4»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }]).sum«1».«5»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum«1».«6»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum«1».«7»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }]).sum«1».«8»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }]).sum«1».«9»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum«1».«10»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum«1».«11»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum«1».«12»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum«1».«13»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum«1».«14»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum«1».«15»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum«1».«16»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 2 }]).sum =
  (↑[{ M := 0, N := 2 }]).sum«1».«17»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 2 }]).sum«1».«18»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 2 }]).sum«1».«19»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 2 }]).sum«1».«20»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 2 }]).sum«1».«21»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 2 }]).sum«1».«22»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 2 }]).sum«1».«23»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 2 }]).sum«1».«24»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 0, N := 1 }, { M := 0, N := 2 }]).sum«1».«25»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum«1».«26»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum«1».«27»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum«1».«28»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum«1».«29»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum«1».«30»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum«1».«31»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum«2».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«2».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }]).sum«2».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }]).sum«2».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum«2».«4»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }]).sum =
  (↑[{ M := 1, N := 0 }]).sum«2».«5»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 1, N := 0 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 1, N := 0 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := 0 }]).sum«2».«6»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 1, N := 0 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 1, N := 0 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := 0 }]).sum«2».«7»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := 0 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := 0 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := 0 }]).sum«2».«8»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }]).sum«2».«9»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum«2».«10»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum«2».«11»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum«2».«12»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 0, N := 1 }]).sum«2».«13»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 1 }]).sum«2».«14»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 1 }]).sum«2».«15»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 1 }]).sum«2».«16»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }]).sum«2».«17»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum«2».«18»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum«2».«19»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum«2».«20»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 0, N := 1 }]).sum«2».«21»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 1 }]).sum«2».«22»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 1 }]).sum«2».«23»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 1 }]).sum«2».«24»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum«2».«25»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«2».«26»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«2».«27»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«2».«28»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := 0 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := 0 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«2».«29»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«2».«30»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«2».«31»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«3».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«3».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 1 }]).sum =
  (↑[{ M := 1, N := 1 }]).sum«3».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }]).sum«3».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 1 }, { M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 1 }, { M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := 1 }, { M := 1, N := -1 }]).sum«3».«4»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }]).sum«3».«5»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 1 }, { M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 1 }, { M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := 1 }, { M := 1, N := -1 }]).sum«3».«6»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum«3».«7»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 1, N := -1 }]).sum«3».«8»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }]).sum«3».«9»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := 1 }, { M := 0, N := 1 }]).sum«3».«10»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum«3».«11»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum«3».«12»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum«3».«13»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum«3».«14»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum«3».«15»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := 1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum«4».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«4».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }]).sum =
  (↑[{ M := 1, N := 0 }]).sum«4».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }]).sum =
  (↑[{ M := 1, N := 0 }]).sum«4».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }, { M := 1, N := 0 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }, { M := 1, N := 0 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 1, N := 0 }]).sum«4».«4»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }]).sum«4».«5»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }, { M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }, { M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 1, N := -1 }]).sum«4».«6»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }, { M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }, { M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 1, N := -1 }]).sum«4».«7»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := 0 }, { M := 1, N := 0 }, { M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := 0 }, { M := 1, N := 0 }, { M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 1, N := 0 }, { M := 1, N := -1 }]).sum«4».«8»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }]).sum«4».«9»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 0, N := 1 }]).sum«4».«10»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 0, N := 1 }]).sum«4».«11»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := 0 }, { M := 1, N := 0 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := 0 }, { M := 1, N := 0 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 1, N := 0 }, { M := 0, N := 1 }]).sum«4».«12»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum«4».«13»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := 0 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := 0 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum«4».«14»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := 0 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := 0 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum«4».«15»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := 0 }, { M := 1, N := 0 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := 0 }, { M := 1, N := 0 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 1, N := 0 }, { M := 1, N := -1 }, { M := 0, N := 1 }]).sum«5».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«5».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }]).sum«5».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }]).sum =
  (↑[{ M := 1, N := 0 }]).sum«5».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 1, N := 0 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 1, N := 0 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := 0 }]).sum«5».«4»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }]).sum«5».«5»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum«5».«6»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }, { M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }, { M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 1, N := -1 }]).sum«5».«7»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 1, N := -1 }]).sum«5».«8»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 2 }]).sum =
  (↑[{ M := 0, N := 2 }]).sum«5».«9»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 2 }]).sum«5».«10»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 0, N := 2 }]).sum«5».«11»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 0, N := 2 }]).sum«5».«12»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 2 }]).sum«5».«13»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 2 }]).sum«5».«14»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := 0 }, { M := 1, N := -1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := 0 }, { M := 1, N := -1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 1, N := -1 }, { M := 0, N := 2 }]).sum«5».«15»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 1, N := -1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 1, N := -1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 1, N := -1 }, { M := 0, N := 2 }]).sum«6».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«6».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }]).sum«6».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }]).sum«6».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum«6».«4»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }]).sum«6».«5»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum«6».«6»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum«6».«7»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }]).sum«6».«8»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 3 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 3 }]).sum =
  (↑[{ M := 0, N := 3 }]).sum«6».«9»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 3 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 3 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 3 }]).sum«6».«10»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 3 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 3 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 3 }]).sum«6».«11»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 3 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 3 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 3 }]).sum«6».«12»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 3 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 3 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 3 }]).sum«6».«13»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 3 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 3 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 3 }]).sum«6».«14»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 3 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 3 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 3 }]).sum«6».«15»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 3 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 3 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := -1 }, { M := 0, N := 3 }]).sum«7».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«7».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }]).sum«7».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }]).sum«7».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }]).sum«7».«4»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 2 }]).sum =
  (↑[{ M := 1, N := 2 }]).sum«7».«5»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 1, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 1, N := 2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := 2 }]).sum«7».«6»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 1, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 1, N := 2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := 2 }]).sum«7».«7»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := 2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := -1 }, { M := 1, N := 2 }]).sum«8».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«8».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }]).sum«8».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }]).sum =
  (↑[{ M := 1, N := 0 }]).sum«8».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 1, N := 0 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 1, N := 0 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := 0 }]).sum«8».«4»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 1 }]).sum =
  (↑[{ M := 1, N := 1 }]).sum«8».«5»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 1, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 1, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := 1 }]).sum«8».«6»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }, { M := 1, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }, { M := 1, N := 1 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 1, N := 1 }]).sum«8».«7»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 1, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 1, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 1, N := 0 }, { M := 1, N := 1 }]).sum«9».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«9».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }]).sum =
  (↑[{ M := 1, N := 0 }]).sum«9».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }]).sum =
  (↑[{ M := 1, N := 0 }]).sum«9».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }, { M := 1, N := 0 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }, { M := 1, N := 0 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 1, N := 0 }]).sum«9».«4»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }]).sum =
  (↑[{ M := 1, N := 0 }]).sum«9».«5»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }, { M := 1, N := 0 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }, { M := 1, N := 0 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 1, N := 0 }]).sum«9».«6»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }, { M := 1, N := 0 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }, { M := 1, N := 0 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 1, N := 0 }]).sum«9».«7»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := 0 }, { M := 1, N := 0 }, { M := 1, N := 0 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := 0 }, { M := 1, N := 0 }, { M := 1, N := 0 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 1, N := 0 }, { M := 1, N := 0 }]).sum«10».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«10».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }]).sum«10».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 2, N := -2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 2, N := -2 }]).sum =
  (↑[{ M := 2, N := -2 }]).sum«10».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 2, N := -2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 2, N := -2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 2, N := -2 }]).sum«10».«4»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }]).sum«10».«5»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum«10».«6»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 2, N := -2 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 2, N := -2 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 2, N := -2 }, { M := 0, N := 1 }]).sum«10».«7»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }]).sum«10».«8»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }]).sum«10».«9»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum«10».«10»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 2, N := -2 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 2, N := -2 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 2, N := -2 }, { M := 0, N := 1 }]).sum«10».«11»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }]).sum«10».«12»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum«10».«13»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«10».«14»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«10».«15»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«10».«16»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }]).sum«10».«17»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum«10».«18»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 2, N := -2 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 2, N := -2 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 2, N := -2 }, { M := 0, N := 1 }]).sum«10».«19»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }]).sum«10».«20»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum«10».«21»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«10».«22»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«10».«23»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«10».«24»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum«10».«25»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«10».«26»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«10».«27»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«10».«28»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«10».«29»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«10».«30»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«10».«31»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«11».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«11».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }]).sum«11».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 2, N := -2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 2, N := -2 }]).sum =
  (↑[{ M := 2, N := -2 }]).sum«11».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 2, N := -2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 2, N := -2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 2, N := -2 }]).sum«11».«4»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }]).sum«11».«5»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum«11».«6»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 2, N := -2 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 2, N := -2 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 2, N := -2 }, { M := 0, N := 1 }]).sum«11».«7»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }]).sum«11».«8»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 2 }]).sum =
  (↑[{ M := 0, N := 2 }]).sum«11».«9»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 2 }]).sum«11».«10»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 2, N := -2 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 2, N := -2 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 2, N := -2 }, { M := 0, N := 2 }]).sum«11».«11»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 2 }]).sum«11».«12»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 0, N := 1 }, { M := 0, N := 2 }]).sum«11».«13»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum«11».«14»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum«11».«15»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum«12».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«12».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }]).sum«12».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 2, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 2, N := -1 }]).sum =
  (↑[{ M := 2, N := -1 }]).sum«12».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 2, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 2, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 2, N := -1 }]).sum«12».«4»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }]).sum«12».«5»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum«12».«6»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 2, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 2, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 2, N := -1 }, { M := 0, N := 1 }]).sum«12».«7»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 2, N := -1 }, { M := 0, N := 1 }]).sum«12».«8»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }]).sum«12».«9»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum«12».«10»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 2, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 2, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 2, N := -1 }, { M := 0, N := 1 }]).sum«12».«11»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 2, N := -1 }, { M := 0, N := 1 }]).sum«12».«12»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum«12».«13»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«12».«14»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 2, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 2, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 2, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«12».«15»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 2, N := -1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«13».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«13».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }]).sum =
  (↑[{ M := 1, N := 0 }]).sum«13».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 2, N := -2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 2, N := -2 }]).sum =
  (↑[{ M := 2, N := -2 }]).sum«13».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }, { M := 2, N := -2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }, { M := 2, N := -2 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 2, N := -2 }]).sum«13».«4»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }]).sum«13».«5»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 0, N := 1 }]).sum«13».«6»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 2, N := -2 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 2, N := -2 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 2, N := -2 }, { M := 0, N := 1 }]).sum«13».«7»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := 0 }, { M := 2, N := -2 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := 0 }, { M := 2, N := -2 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 2, N := -2 }, { M := 0, N := 1 }]).sum«13».«8»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }]).sum«13».«9»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 0, N := 1 }]).sum«13».«10»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 2, N := -2 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 2, N := -2 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 2, N := -2 }, { M := 0, N := 1 }]).sum«13».«11»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := 0 }, { M := 2, N := -2 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := 0 }, { M := 2, N := -2 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 2, N := -2 }, { M := 0, N := 1 }]).sum«13».«12»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum«13».«13»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := 0 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := 0 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«13».«14»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«13».«15»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := 0 }, { M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := 0 }, { M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 2, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«14».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«14».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 1 }]).sum =
  (↑[{ M := 1, N := 1 }]).sum«14».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 2, N := -2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 2, N := -2 }]).sum =
  (↑[{ M := 2, N := -2 }]).sum«14».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 1 }, { M := 2, N := -2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 1 }, { M := 2, N := -2 }]).sum =
  (↑[{ M := 1, N := 1 }, { M := 2, N := -2 }]).sum«14».«4»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }]).sum«14».«5»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := 1 }, { M := 0, N := 1 }]).sum«14».«6»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 2, N := -2 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 2, N := -2 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 2, N := -2 }, { M := 0, N := 1 }]).sum«14».«7»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := 1 }, { M := 2, N := -2 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := 1 }, { M := 2, N := -2 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := 1 }, { M := 2, N := -2 }, { M := 0, N := 1 }]).sum«15».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«15».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }]).sum =
  (↑[{ M := 1, N := 0 }]).sum«15».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 2, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 2, N := -1 }]).sum =
  (↑[{ M := 2, N := -1 }]).sum«15».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }, { M := 2, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }, { M := 2, N := -1 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 2, N := -1 }]).sum«15».«4»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }]).sum«15».«5»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 0, N := 1 }]).sum«15».«6»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 2, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 2, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 2, N := -1 }, { M := 0, N := 1 }]).sum«15».«7»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := 0 }, { M := 2, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := 0 }, { M := 2, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 2, N := -1 }, { M := 0, N := 1 }]).sum«16».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«16».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }]).sum =
  (↑[{ M := 1, N := 0 }]).sum«16».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 2, N := -2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 2, N := -2 }]).sum =
  (↑[{ M := 2, N := -2 }]).sum«16».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }, { M := 2, N := -2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }, { M := 2, N := -2 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 2, N := -2 }]).sum«16».«4»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 2 }]).sum =
  (↑[{ M := 0, N := 2 }]).sum«16».«5»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 0, N := 2 }]).sum«16».«6»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 2, N := -2 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 2, N := -2 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 2, N := -2 }, { M := 0, N := 2 }]).sum«16».«7»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := 0 }, { M := 2, N := -2 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := 0 }, { M := 2, N := -2 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 2, N := -2 }, { M := 0, N := 2 }]).sum«17».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«17».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }]).sum«17».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 2, N := 0 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 2, N := 0 }]).sum =
  (↑[{ M := 2, N := 0 }]).sum«17».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 2, N := 0 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 2, N := 0 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 2, N := 0 }]).sum«17».«4»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }]).sum«17».«5»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 1 }]).sum«17».«6»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 2, N := 0 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 2, N := 0 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 2, N := 0 }, { M := 0, N := 1 }]).sum«17».«7»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := 0 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := 0 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 2, N := 0 }, { M := 0, N := 1 }]).sum«18».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«18».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }]).sum«18».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 2, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 2, N := -1 }]).sum =
  (↑[{ M := 2, N := -1 }]).sum«18».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 2, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 2, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 2, N := -1 }]).sum«18».«4»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 2 }]).sum =
  (↑[{ M := 0, N := 2 }]).sum«18».«5»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 2 }]).sum«18».«6»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 2, N := -1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 2, N := -1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 2, N := -1 }, { M := 0, N := 2 }]).sum«18».«7»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 2, N := -1 }, { M := 0, N := 2 }]).sum«19».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«19».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }]).sum«19».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 2, N := -2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 2, N := -2 }]).sum =
  (↑[{ M := 2, N := -2 }]).sum«19».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 2, N := -2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 2, N := -2 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 2, N := -2 }]).sum«19».«4»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 3 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 3 }]).sum =
  (↑[{ M := 0, N := 3 }]).sum«19».«5»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 3 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 0, N := 3 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 0, N := 3 }]).sum«19».«6»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 2, N := -2 }, { M := 0, N := 3 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 2, N := -2 }, { M := 0, N := 3 }]).sum =
  (↑[{ M := 2, N := -2 }, { M := 0, N := 3 }]).sum«19».«7»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 3 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 3 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 2, N := -2 }, { M := 0, N := 3 }]).sum«20».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«20».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }]).sum =
  (↑[{ M := 1, N := -1 }]).sum«20».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 2, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 2, N := 1 }]).sum =
  (↑[{ M := 2, N := 1 }]).sum«20».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := -1 }, { M := 2, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := -1 }, { M := 2, N := 1 }]).sum =
  (↑[{ M := 1, N := -1 }, { M := 2, N := 1 }]).sum«21».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«21».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }]).sum =
  (↑[{ M := 1, N := 0 }]).sum«21».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 2, N := 0 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 2, N := 0 }]).sum =
  (↑[{ M := 2, N := 0 }]).sum«21».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 0 }, { M := 2, N := 0 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 0 }, { M := 2, N := 0 }]).sum =
  (↑[{ M := 1, N := 0 }, { M := 2, N := 0 }]).sum«22».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«22».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 1 }]).sum =
  (↑[{ M := 1, N := 1 }]).sum«22».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 2, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 2, N := -1 }]).sum =
  (↑[{ M := 2, N := -1 }]).sum«22».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 1 }, { M := 2, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 1 }, { M := 2, N := -1 }]).sum =
  (↑[{ M := 1, N := 1 }, { M := 2, N := -1 }]).sum«23».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«23».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 2 }]).sum =
  (↑[{ M := 1, N := 2 }]).sum«23».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 2, N := -2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 2, N := -2 }]).sum =
  (↑[{ M := 2, N := -2 }]).sum«23».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 1, N := 2 }, { M := 2, N := -2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 1, N := 2 }, { M := 2, N := -2 }]).sum =
  (↑[{ M := 1, N := 2 }, { M := 2, N := -2 }]).sum«24».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«24».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 3, N := -3 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 3, N := -3 }]).sum =
  (↑[{ M := 3, N := -3 }]).sum«24».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }]).sum«24».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 3, N := -3 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 3, N := -3 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 3, N := -3 }, { M := 0, N := 1 }]).sum«24».«4»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }]).sum«24».«5»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 3, N := -3 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 3, N := -3 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 3, N := -3 }, { M := 0, N := 1 }]).sum«24».«6»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum«24».«7»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 3, N := -3 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 3, N := -3 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 3, N := -3 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«24».«8»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }]).sum«24».«9»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 3, N := -3 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 3, N := -3 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 3, N := -3 }, { M := 0, N := 1 }]).sum«24».«10»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum«24».«11»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 3, N := -3 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 3, N := -3 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 3, N := -3 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«24».«12»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum«24».«13»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 3, N := -3 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 3, N := -3 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 3, N := -3 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«24».«14»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«24».«15»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 3, N := -3 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 3, N := -3 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 3, N := -3 }, { M := 0, N := 1 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«25».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«25».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 3, N := -3 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 3, N := -3 }]).sum =
  (↑[{ M := 3, N := -3 }]).sum«25».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }]).sum«25».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 3, N := -3 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 3, N := -3 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 3, N := -3 }, { M := 0, N := 1 }]).sum«25».«4»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 2 }]).sum =
  (↑[{ M := 0, N := 2 }]).sum«25».«5»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 3, N := -3 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 3, N := -3 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 3, N := -3 }, { M := 0, N := 2 }]).sum«25».«6»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 0, N := 1 }, { M := 0, N := 2 }]).sum«25».«7»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 3, N := -3 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 3, N := -3 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 3, N := -3 }, { M := 0, N := 1 }, { M := 0, N := 2 }]).sum«26».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«26».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 3, N := -2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 3, N := -2 }]).sum =
  (↑[{ M := 3, N := -2 }]).sum«26».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }]).sum«26».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 3, N := -2 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 3, N := -2 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 3, N := -2 }, { M := 0, N := 1 }]).sum«26».«4»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }]).sum«26».«5»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 3, N := -2 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 3, N := -2 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 3, N := -2 }, { M := 0, N := 1 }]).sum«26».«6»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }, { M := 0, N := 1 }]).sum«26».«7»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| })
        ↑[{ M := 3, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| })
        ↑[{ M := 3, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 3, N := -2 }, { M := 0, N := 1 }, { M := 0, N := 1 }]).sum«27».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«27».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 3, N := -3 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 3, N := -3 }]).sum =
  (↑[{ M := 3, N := -3 }]).sum«27».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 3 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 3 }]).sum =
  (↑[{ M := 0, N := 3 }]).sum«27».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 3, N := -3 }, { M := 0, N := 3 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 3, N := -3 }, { M := 0, N := 3 }]).sum =
  (↑[{ M := 3, N := -3 }, { M := 0, N := 3 }]).sum«28».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«28».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 3, N := -2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 3, N := -2 }]).sum =
  (↑[{ M := 3, N := -2 }]).sum«28».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 2 }]).sum =
  (↑[{ M := 0, N := 2 }]).sum«28».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 3, N := -2 }, { M := 0, N := 2 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 3, N := -2 }, { M := 0, N := 2 }]).sum =
  (↑[{ M := 3, N := -2 }, { M := 0, N := 2 }]).sum«29».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«29».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 3, N := -1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 3, N := -1 }]).sum =
  (↑[{ M := 3, N := -1 }]).sum«29».«2»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 0, N := 1 }]).sum =
  (↑[{ M := 0, N := 1 }]).sum«29».«3»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 3, N := -1 }, { M := 0, N := 1 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 3, N := -1 }, { M := 0, N := 1 }]).sum =
  (↑[{ M := 3, N := -1 }, { M := 0, N := 1 }]).sum«30».«0»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[]).sum =
  (↑[]).sum«30».«1»⊢ (Multiset.map (fun x => { M := |x.M|, N := -|x.M| }) ↑[{ M := 3, N := 0 }]).sum +
    (Multiset.map (fun x => { M := 0, N := |x.M + x.N| }) ↑[{ M := 3, N := 0 }]).sum =
  (↑[{ M := 3, N := 0 }]).sum decideAll goals completed! 🐙

B. The multiset sets of `FluxesFive` with no chiral exotics and no zero fluxes

B.1. The definition of the multiset

The elements of FluxesTen for which the NoExotics condition holds.

def elemsNoExotics : Multiset FluxesTen := {{⟨1, 0⟩, ⟨1, 0⟩, ⟨1, 0⟩},
  {⟨1, 1⟩, ⟨1, -1⟩, ⟨1, 0⟩}, {⟨1, 0⟩, ⟨2, 0⟩},
  {⟨1, -1⟩, ⟨2, 1⟩}, {⟨1, 1⟩, ⟨2, -1⟩},
  {⟨3, 0⟩}}

B.2. The cardinality of the multiset is 6

lemma elemsNoExotics_card : elemsNoExotics.card = 6 := by⊢ elemsNoExotics.card = 6
  decideAll goals completed! 🐙

B.3. The multiset has no duplicates

lemma elemsNoExotics_nodup : elemsNoExotics.Nodup := by⊢ elemsNoExotics.Nodup
  decideAll goals completed! 🐙

B.4. Every element of the multiset obeys `NoExotics`

lemma noExotics_of_mem_elemsNoExotics (F : FluxesTen) (h : F ∈ elemsNoExotics) :
    NoExotics F := byF:FluxesTenh:F ∈ elemsNoExotics⊢ F.NoExotics
  revert F⊢ ∀ F ∈ elemsNoExotics, F.NoExotics
  decideAll goals completed! 🐙

B.5. Every element of the multiset has at most 3 distinct flux pairs

lemma toFinset_card_le_three_mem_elemsNoExotics (F : FluxesTen) (h : F ∈ elemsNoExotics) :
    F.toFinset.card ≤ 3 := byF:FluxesTenh:F ∈ elemsNoExotics⊢ (Multiset.toFinset F).card ≤ 3
  revert F h⊢ ∀ F ∈ elemsNoExotics, (Multiset.toFinset F).card ≤ 3
  decideAll goals completed! 🐙

B.6. The sum of all flux-pairs in any element of the multiset is (3, 0)

lemma sum_of_mem_elemsNoExotics (F : FluxesTen) (h : F ∈ elemsNoExotics) :
    F.sum = ⟨3, 0⟩ := byF:FluxesTenh:F ∈ elemsNoExotics⊢ Multiset.sum F = { M := 3, N := 0 }
  revert F h⊢ ∀ F ∈ elemsNoExotics, Multiset.sum F = { M := 3, N := 0 }
  decideAll goals completed! 🐙

B.7. Every element of the multiset obeys `HasNoZero`

lemma hasNoZero_of_mem_elemsNoExotics (F : FluxesTen) (h : F ∈ elemsNoExotics) :
    F.HasNoZero := byF:FluxesTenh:F ∈ elemsNoExotics⊢ F.HasNoZero
  revert F h⊢ ∀ F ∈ elemsNoExotics, F.HasNoZero
  decideAll goals completed! 🐙

Terms of FluxesFive and FluxesTen with no chiral exotics

i. Overview

ii. Key results

iii. Table of contents

iv. References

A. The multiset sets of FluxesFive with no chiral exotics and no zero fluxes

A.1. The definition of the multiset

A.2. The cardinality of the multiset is 31

A.3. The multiset has no duplicates

A.4. Every element of the multiset obeys NoExotics

A.5. Every element of the multiset has at most 4 distinct flux pairs

A.6. Every element of the multiset has at most 6 flux pairs

A.7. The sum of all flux-pairs in any element of the multiset is (3, 0)

A.8. Every element of the multiset obeys HasNoZero

A.9. A sum relation for subsets of elements of the multiset

B. The multiset sets of FluxesFive with no chiral exotics and no zero fluxes

B.1. The definition of the multiset

B.2. The cardinality of the multiset is 6

B.3. The multiset has no duplicates

B.4. Every element of the multiset obeys NoExotics

B.5. Every element of the multiset has at most 3 distinct flux pairs

B.6. The sum of all flux-pairs in any element of the multiset is (3, 0)

B.7. Every element of the multiset obeys HasNoZero

Terms of `FluxesFive` and `FluxesTen` with no chiral exotics

A. The multiset sets of `FluxesFive` with no chiral exotics and no zero fluxes

A.4. Every element of the multiset obeys `NoExotics`

A.8. Every element of the multiset obeys `HasNoZero`

B. The multiset sets of `FluxesFive` with no chiral exotics and no zero fluxes

B.4. Every element of the multiset obeys `NoExotics`

B.7. Every element of the multiset obeys `HasNoZero`