EI0025

eisenstein_product_associate_imaginary

Imaginary Eisenstein associativity follows constructively from real associativity under the exact ω rotation, avoiding an oversized polynomial expansion.

Alpha v34 checked-use · first admitted v28 · independently kernel and Lean verified; not Stable

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

A floor quotient in the fundamental parallelogram already gives the required strict norm decrease; global nearest-point optimality is not asserted. The shared carrier is identical to the Gaussian carrier, but the multiplication law and norm are different. Eisenstein gcd, factorization, and prime classification remain separate targets.

Exact theorem in conservative defined notation

∀ a. ∀ b. ∀ c. ∀ d. ∀ e. ∀ f. ∀ g. ∀ h. ∀ i. ∀ j. ∀ k. ∀ l. (a · e + b · f + (c · h + d · g)) · k + (a · f + b · e + (c · g + d · h)) · l + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · i + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · j) + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · l + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · k) + (a · (e · l + f · k + (g · j + h · i) + (g · k + h · l)) + b · (e · k + f · l + (g · i + h · j) + (g · l + h · k)) + (c · (e · j + f · i + (g · k + h · l)) + d · (e · i + f · j + (g · l + h · k))) + (c · (e · k + f · l + (g · i + h · j) + (g · l + h · k)) + d · (e · l + f · k + (g · j + h · i) + (g · k + h · l)))) = a · (e · k + f · l + (g · i + h · j) + (g · l + h · k)) + b · (e · l + f · k + (g · j + h · i) + (g · k + h · l)) + (c · (e · i + f · j + (g · l + h · k)) + d · (e · j + f · i + (g · k + h · l))) + (c · (e · l + f · k + (g · j + h · i) + (g · k + h · l)) + d · (e · k + f · l + (g · i + h · j) + (g · l + h · k))) + ((a · e + b · f + (c · h + d · g)) · l + (a · f + b · e + (c · g + d · h)) · k + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · j + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · i) + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · k + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · l))

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

EisensteinCoordinateProduct(ap,an,bp,bn,cp,cn,dp,dn,rp,rn,sp,sn) · 3

Actual proof prerequisites

eisenstein_product_integer_congruenceeisenstein_omega_product_covariancegaussian_equal_reflexive · checked external prerequisiteinteger_span_pair_equal_transitive · checked external prerequisiteeisenstein_product_associate_realmatrix_integer_pair_negation_balance · checked external prerequisite
Original expanded first-order statement 
forall a b c d e f g h i j k l. ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (k))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (l))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (i))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (j))))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (l))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (k))))))) + (((((((((a) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((b) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))))) + (((((c) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((d) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))))) + (((((c) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((d) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l)))))))))))))) = ((((((((((a) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((b) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))))) + (((((c) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((d) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))))) + (((((c) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((d) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))))))) + (((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (l))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (k))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (j))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (i))))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (k))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (l))))))))

Complete tactic proof in conservative notation

All 116 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

116 script commands · 16 reading checkpoints · 6 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (3)
eisenstein product integer congruenceeisenstein omega product covarianceeisenstein product associate real
01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro d
  5. L5
    intro e
  6. L6
    intro f
  7. L7
    intro g
  8. L8
    intro h
  9. L9
    intro i
  10. L10
    intro j
02Fix variables and assumptionsL11–12

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro k
  2. L12
    intro l
03Establish hfirstL13–22

Establish this local claim before using it. It is not an additional assumption.

  1. L13
    have hfirst · expand full local formula (1,882 characters)have hfirst : EisensteinCoordinateProduct(d · e + c · f + ((a + d) · h + (b + c) · g),d · f + c · e + ((a + d) · g + (b + c) · h),d · g + c · h + ((a + d) · e + (b + c) · f) + ((a + d) · h + (b + c) · g),d · h + c · g + ((a + d) · f + (b + c) · e) + ((a + d) · g + (b + c) · h),i,j,k,l,(a · h + b · g + (c · f + d · e) + (c · g + d · h)) · i + (a · g + b · h + (c · e + d · f) + (c · h + d · g)) · j + ((a · e + b · f + (c · h + d · g) + (a · h + b · g + (c · f + d · e) + (c · g + d · h))) · l + (a · f + b · e + (c · g + d · h) + (a · g + b · h + (c · e + d · f) + (c · h + d · g))) · k),(a · h + b · g + (c · f + d · e) + (c · g + d · h)) · j + (a · g + b · h + (c · e + d · f) + (c · h + d · g)) · i + ((a · e + b · f + (c · h + d · g) + (a · h + b · g + (c · f + d · e) + (c · g + d · h))) · k + (a · f + b · e + (c · g + d · h) + (a · g + b · h + (c · e + d · f) + (c · h + d · g))) · l),(a · h + b · g + (c · f + d · e) + (c · g + d · h)) · k + (a · g + b · h + (c · e + d · f) + (c · h + d · g)) · l + ((a · e + b · f + (c · h + d · g) + (a · h + b · g + (c · f + d · e) + (c · g + d · h))) · i + (a · f + b · e + (c · g + d · h) + (a · g + b · h + (c · e + d · f) + (c · h + d · g))) · j) + ((a · e + b · f + (c · h + d · g) + (a · h + b · g + (c · f + d · e) + (c · g + d · h))) · l + (a · f + b · e + (c · g + d · h) + (a · g + b · h + (c · e + d · f) + (c · h + d · g))) · k),(a · h + b · g + (c · f + d · e) + (c · g + d · h)) · l + (a · g + b · h + (c · e + d · f) + (c · h + d · g)) · k + ((a · e + b · f + (c · h + d · g) + (a · h + b · g + (c · f + d · e) + (c · g + d · h))) · j + (a · f + b · e + (c · g + d · h) + (a · g + b · h + (c · e + d · f) + (c · h + d · g))) · i) + ((a · e + b · f + (c · h + d · g) + (a · h + b · g + (c · f + d · e) + (c · g + d · h))) · k + (a · f + b · e + (c · g + d · h) + (a · g + b · h + (c · e + d · f) + (c · h + d · g))) · l))
    Definitions: EisensteinCoordinateProduct(d · e + c · f + ((a + d) · h + (b + c) · g),d · f + c · e + ((a + d) · g + (b + c) · h),d · g + c · h + ((a + d) · e + (b + c) · f) + ((a + d) · h + (b + c) · g),d · h + c · g + ((a + d) · f + (b + c) · e) + ((a + d) · g + (b + c) · h),i,j,k,l,(a · h + b · g + (c · f + d · e) + (c · g + d · h)) · i + (a · g + b · h + (c · e + d · f) + (c · h + d · g)) · j + ((a · e + b · f + (c · h + d · g) + (a · h + b · g + (c · f + d · e) + (c · g + d · h))) · l + (a · f + b · e + (c · g + d · h) + (a · g + b · h + (c · e + d · f) + (c · h + d · g))) · k),(a · h + b · g + (c · f + d · e) + (c · g + d · h)) · j + (a · g + b · h + (c · e + d · f) + (c · h + d · g)) · i + ((a · e + b · f + (c · h + d · g) + (a · h + b · g + (c · f + d · e) + (c · g + d · h))) · k + (a · f + b · e + (c · g + d · h) + (a · g + b · h + (c · e + d · f) + (c · h + d · g))) · l),(a · h + b · g + (c · f + d · e) + (c · g + d · h)) · k + (a · g + b · h + (c · e + d · f) + (c · h + d · g)) · l + ((a · e + b · f + (c · h + d · g) + (a · h + b · g + (c · f + d · e) + (c · g + d · h))) · i + (a · f + b · e + (c · g + d · h) + (a · g + b · h + (c · e + d · f) + (c · h + d · g))) · j) + ((a · e + b · f + (c · h + d · g) + (a · h + b · g + (c · f + d · e) + (c · g + d · h))) · l + (a · f + b · e + (c · g + d · h) + (a · g + b · h + (c · e + d · f) + (c · h + d · g))) · k),(a · h + b · g + (c · f + d · e) + (c · g + d · h)) · l + (a · g + b · h + (c · e + d · f) + (c · h + d · g)) · k + ((a · e + b · f + (c · h + d · g) + (a · h + b · g + (c · f + d · e) + (c · g + d · h))) · j + (a · f + b · e + (c · g + d · h) + (a · g + b · h + (c · e + d · f) + (c · h + d · g))) · i) + ((a · e + b · f + (c · h + d · g) + (a · h + b · g + (c · f + d · e) + (c · g + d · h))) · k + (a · f + b · e + (c · g + d · h) + (a · g + b · h + (c · e + d · f) + (c · h + d · g))) · l))Original native command in the exact edition
  2. L14
    specialize eisenstein_product_integer_congruence ((((((d) * (e))) + (((c) * (f))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))
  3. L15
    specialize eisenstein_product_integer_congruence ((((((d) * (f))) + (((c) * (e))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))
  4. L16
    specialize eisenstein_product_integer_congruence ((((((((d) * (g))) + (((c) * (h))))) + (((((((a) + (d))) * (e))) + (((((b) + (c))) * (f))))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))
  5. L17
    specialize eisenstein_product_integer_congruence ((((((((d) * (h))) + (((c) * (g))))) + (((((((a) + (d))) * (f))) + (((((b) + (c))) * (e))))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))
  6. L18
    specialize eisenstein_product_integer_congruence ((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))
  7. L19
    specialize eisenstein_product_integer_congruence ((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))
  8. L20
    specialize eisenstein_product_integer_congruence ((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))
  9. L21
    specialize eisenstein_product_integer_congruence ((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))
  10. L22
    specialize eisenstein_product_integer_congruence i
04Use earlier factsL23–32

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L23
    specialize eisenstein_product_integer_congruence j
  2. L24
    specialize eisenstein_product_integer_congruence k
  3. L25
    specialize eisenstein_product_integer_congruence l
  4. L26
    specialize eisenstein_product_integer_congruence i
  5. L27
    specialize eisenstein_product_integer_congruence j
  6. L28
    specialize eisenstein_product_integer_congruence k
  7. L29
    specialize eisenstein_product_integer_congruence l
  8. L30
    apply eisenstein_product_integer_congruence
  9. L31
    specialize eisenstein_omega_product_covariance a
  10. L32
    specialize eisenstein_omega_product_covariance b
05Use earlier factsL33–42

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L33
    specialize eisenstein_omega_product_covariance c
  2. L34
    specialize eisenstein_omega_product_covariance d
  3. L35
    specialize eisenstein_omega_product_covariance e
  4. L36
    specialize eisenstein_omega_product_covariance f
  5. L37
    specialize eisenstein_omega_product_covariance g
  6. L38
    specialize eisenstein_omega_product_covariance h
  7. L39
    apply eisenstein_omega_product_covariance
  8. L40
    specialize gaussian_equal_reflexive i
  9. L41
    specialize gaussian_equal_reflexive j
  10. L42
    specialize gaussian_equal_reflexive k
06Use earlier factsL43–44

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L43
    specialize gaussian_equal_reflexive l
  2. L44
    apply gaussian_equal_reflexive
07Establish hrotationL45–54

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eisenstein omega product covariance.

  1. L45
    have hrotation · expand full local formula (1,981 characters)have hrotation : EisensteinCoordinateProduct(a · h + b · g + (c · f + d · e) + (c · g + d · h),a · g + b · h + (c · e + d · f) + (c · h + d · g),a · e + b · f + (c · h + d · g) + (a · h + b · g + (c · f + d · e) + (c · g + d · h)),a · f + b · e + (c · g + d · h) + (a · g + b · h + (c · e + d · f) + (c · h + d · g)),i,j,k,l,(a · e + b · f + (c · h + d · g)) · l + (a · f + b · e + (c · g + d · h)) · k + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · j + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · i) + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · k + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · l),(a · e + b · f + (c · h + d · g)) · k + (a · f + b · e + (c · g + d · h)) · l + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · i + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · j) + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · l + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · k),(a · e + b · f + (c · h + d · g)) · i + (a · f + b · e + (c · g + d · h)) · j + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · l + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · k) + ((a · e + b · f + (c · h + d · g)) · l + (a · f + b · e + (c · g + d · h)) · k + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · j + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · i) + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · k + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · l)),(a · e + b · f + (c · h + d · g)) · j + (a · f + b · e + (c · g + d · h)) · i + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · k + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · l) + ((a · e + b · f + (c · h + d · g)) · k + (a · f + b · e + (c · g + d · h)) · l + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · i + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · j) + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · l + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · k)))
    Definitions: EisensteinCoordinateProduct(a · h + b · g + (c · f + d · e) + (c · g + d · h),a · g + b · h + (c · e + d · f) + (c · h + d · g),a · e + b · f + (c · h + d · g) + (a · h + b · g + (c · f + d · e) + (c · g + d · h)),a · f + b · e + (c · g + d · h) + (a · g + b · h + (c · e + d · f) + (c · h + d · g)),i,j,k,l,(a · e + b · f + (c · h + d · g)) · l + (a · f + b · e + (c · g + d · h)) · k + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · j + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · i) + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · k + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · l),(a · e + b · f + (c · h + d · g)) · k + (a · f + b · e + (c · g + d · h)) · l + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · i + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · j) + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · l + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · k),(a · e + b · f + (c · h + d · g)) · i + (a · f + b · e + (c · g + d · h)) · j + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · l + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · k) + ((a · e + b · f + (c · h + d · g)) · l + (a · f + b · e + (c · g + d · h)) · k + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · j + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · i) + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · k + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · l)),(a · e + b · f + (c · h + d · g)) · j + (a · f + b · e + (c · g + d · h)) · i + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · k + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · l) + ((a · e + b · f + (c · h + d · g)) · k + (a · f + b · e + (c · g + d · h)) · l + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · i + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · j) + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · l + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · k)))Original native command in the exact edition
  2. L46
    specialize eisenstein_omega_product_covariance ((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))
  3. L47
    specialize eisenstein_omega_product_covariance ((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))
  4. L48
    specialize eisenstein_omega_product_covariance ((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))
  5. L49
    specialize eisenstein_omega_product_covariance ((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))
  6. L50
    specialize eisenstein_omega_product_covariance i
  7. L51
    specialize eisenstein_omega_product_covariance j
  8. L52
    specialize eisenstein_omega_product_covariance k
  9. L53
    specialize eisenstein_omega_product_covariance l
  10. L54
    apply eisenstein_omega_product_covariance
08Establish hlastL55–64

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eisenstein omega product covariance.

  1. L55
    have hlast · expand full local formula (1,877 characters)have hlast : EisensteinCoordinateProduct(d,c,a + d,b + c,e · i + f · j + (g · l + h · k),e · j + f · i + (g · k + h · l),e · k + f · l + (g · i + h · j) + (g · l + h · k),e · l + f · k + (g · j + h · i) + (g · k + h · l),a · (e · l + f · k + (g · j + h · i) + (g · k + h · l)) + b · (e · k + f · l + (g · i + h · j) + (g · l + h · k)) + (c · (e · j + f · i + (g · k + h · l)) + d · (e · i + f · j + (g · l + h · k))) + (c · (e · k + f · l + (g · i + h · j) + (g · l + h · k)) + d · (e · l + f · k + (g · j + h · i) + (g · k + h · l))),a · (e · k + f · l + (g · i + h · j) + (g · l + h · k)) + b · (e · l + f · k + (g · j + h · i) + (g · k + h · l)) + (c · (e · i + f · j + (g · l + h · k)) + d · (e · j + f · i + (g · k + h · l))) + (c · (e · l + f · k + (g · j + h · i) + (g · k + h · l)) + d · (e · k + f · l + (g · i + h · j) + (g · l + h · k))),a · (e · i + f · j + (g · l + h · k)) + b · (e · j + f · i + (g · k + h · l)) + (c · (e · l + f · k + (g · j + h · i) + (g · k + h · l)) + d · (e · k + f · l + (g · i + h · j) + (g · l + h · k))) + (a · (e · l + f · k + (g · j + h · i) + (g · k + h · l)) + b · (e · k + f · l + (g · i + h · j) + (g · l + h · k)) + (c · (e · j + f · i + (g · k + h · l)) + d · (e · i + f · j + (g · l + h · k))) + (c · (e · k + f · l + (g · i + h · j) + (g · l + h · k)) + d · (e · l + f · k + (g · j + h · i) + (g · k + h · l)))),a · (e · j + f · i + (g · k + h · l)) + b · (e · i + f · j + (g · l + h · k)) + (c · (e · k + f · l + (g · i + h · j) + (g · l + h · k)) + d · (e · l + f · k + (g · j + h · i) + (g · k + h · l))) + (a · (e · k + f · l + (g · i + h · j) + (g · l + h · k)) + b · (e · l + f · k + (g · j + h · i) + (g · k + h · l)) + (c · (e · i + f · j + (g · l + h · k)) + d · (e · j + f · i + (g · k + h · l))) + (c · (e · l + f · k + (g · j + h · i) + (g · k + h · l)) + d · (e · k + f · l + (g · i + h · j) + (g · l + h · k)))))
    Definitions: EisensteinCoordinateProduct(d,c,a + d,b + c,e · i + f · j + (g · l + h · k),e · j + f · i + (g · k + h · l),e · k + f · l + (g · i + h · j) + (g · l + h · k),e · l + f · k + (g · j + h · i) + (g · k + h · l),a · (e · l + f · k + (g · j + h · i) + (g · k + h · l)) + b · (e · k + f · l + (g · i + h · j) + (g · l + h · k)) + (c · (e · j + f · i + (g · k + h · l)) + d · (e · i + f · j + (g · l + h · k))) + (c · (e · k + f · l + (g · i + h · j) + (g · l + h · k)) + d · (e · l + f · k + (g · j + h · i) + (g · k + h · l))),a · (e · k + f · l + (g · i + h · j) + (g · l + h · k)) + b · (e · l + f · k + (g · j + h · i) + (g · k + h · l)) + (c · (e · i + f · j + (g · l + h · k)) + d · (e · j + f · i + (g · k + h · l))) + (c · (e · l + f · k + (g · j + h · i) + (g · k + h · l)) + d · (e · k + f · l + (g · i + h · j) + (g · l + h · k))),a · (e · i + f · j + (g · l + h · k)) + b · (e · j + f · i + (g · k + h · l)) + (c · (e · l + f · k + (g · j + h · i) + (g · k + h · l)) + d · (e · k + f · l + (g · i + h · j) + (g · l + h · k))) + (a · (e · l + f · k + (g · j + h · i) + (g · k + h · l)) + b · (e · k + f · l + (g · i + h · j) + (g · l + h · k)) + (c · (e · j + f · i + (g · k + h · l)) + d · (e · i + f · j + (g · l + h · k))) + (c · (e · k + f · l + (g · i + h · j) + (g · l + h · k)) + d · (e · l + f · k + (g · j + h · i) + (g · k + h · l)))),a · (e · j + f · i + (g · k + h · l)) + b · (e · i + f · j + (g · l + h · k)) + (c · (e · k + f · l + (g · i + h · j) + (g · l + h · k)) + d · (e · l + f · k + (g · j + h · i) + (g · k + h · l))) + (a · (e · k + f · l + (g · i + h · j) + (g · l + h · k)) + b · (e · l + f · k + (g · j + h · i) + (g · k + h · l)) + (c · (e · i + f · j + (g · l + h · k)) + d · (e · j + f · i + (g · k + h · l))) + (c · (e · l + f · k + (g · j + h · i) + (g · k + h · l)) + d · (e · k + f · l + (g · i + h · j) + (g · l + h · k)))))Original native command in the exact edition
  2. L56
    specialize eisenstein_omega_product_covariance a
  3. L57
    specialize eisenstein_omega_product_covariance b
  4. L58
    specialize eisenstein_omega_product_covariance c
  5. L59
    specialize eisenstein_omega_product_covariance d
  6. L60
    specialize eisenstein_omega_product_covariance ((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))
  7. L61
    specialize eisenstein_omega_product_covariance ((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))
  8. L62
    specialize eisenstein_omega_product_covariance ((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))
  9. L63
    specialize eisenstein_omega_product_covariance ((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))
  10. L64
    apply eisenstein_omega_product_covariance
09Separate the logical casesL65–67

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L65
    cases hfirst
  2. L66
    cases hrotation
  3. L67
    cases hlast
10Establish hnegativeL68–68

Establish this local claim before using it. It is not an additional assumption.

  1. L68
    have hnegative · expand full local formula (2,802 characters)have hnegative : ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (l))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (k))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (j))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (i))))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (k))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (l))))))) + (((((((((a) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((b) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))))) + (((((c) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((d) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))))) + (((((c) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((d) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k)))))))))))))) = ((((((((((a) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((b) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))))) + (((((c) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((d) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))))) + (((((c) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((d) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))))))) + (((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (k))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (l))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (i))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (j))))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (l))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (k))))))))
11Establish hleftL69–78

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply integer span pair equal transitive.

  1. L69
    have hleft · expand full local formula (2,518 characters)have hleft : ((((((((((((((d) * (e))) + (((c) * (f))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (i))) + (((((((((d) * (f))) + (((c) * (e))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (j))))) + (((((((((((((d) * (g))) + (((c) * (h))))) + (((((((a) + (d))) * (e))) + (((((b) + (c))) * (f))))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (l))) + (((((((((((d) * (h))) + (((c) * (g))))) + (((((((a) + (d))) * (f))) + (((((b) + (c))) * (e))))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (k))))))) + (((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (k))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (l))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (i))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (j))))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (l))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (k)))))))) = ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (l))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (k))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (j))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (i))))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (k))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (l))))))) + (((((((((((((d) * (e))) + (((c) * (f))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (j))) + (((((((((d) * (f))) + (((c) * (e))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (i))))) + (((((((((((((d) * (g))) + (((c) * (h))))) + (((((((a) + (d))) * (e))) + (((((b) + (c))) * (f))))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (k))) + (((((((((((d) * (h))) + (((c) * (g))))) + (((((((a) + (d))) * (f))) + (((((b) + (c))) * (e))))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (l))))))))
  2. L70
    specialize integer_span_pair_equal_transitive ((((((((((((d) * (e))) + (((c) * (f))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (i))) + (((((((((d) * (f))) + (((c) * (e))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (j))))) + (((((((((((((d) * (g))) + (((c) * (h))))) + (((((((a) + (d))) * (e))) + (((((b) + (c))) * (f))))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (l))) + (((((((((((d) * (h))) + (((c) * (g))))) + (((((((a) + (d))) * (f))) + (((((b) + (c))) * (e))))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (k))))))
  3. L71
    specialize integer_span_pair_equal_transitive ((((((((((((d) * (e))) + (((c) * (f))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (j))) + (((((((((d) * (f))) + (((c) * (e))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (i))))) + (((((((((((((d) * (g))) + (((c) * (h))))) + (((((((a) + (d))) * (e))) + (((((b) + (c))) * (f))))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (k))) + (((((((((((d) * (h))) + (((c) * (g))))) + (((((((a) + (d))) * (f))) + (((((b) + (c))) * (e))))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (l))))))
  4. L72
    specialize integer_span_pair_equal_transitive ((((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (( · expand full local formula (717 characters)specialize integer_span_pair_equal_transitive ((((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (i))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (j))))) + (((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (l))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (k))))))
  5. L73
    specialize integer_span_pair_equal_transitive ((((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (( · expand full local formula (717 characters)specialize integer_span_pair_equal_transitive ((((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (j))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (i))))) + (((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (k))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (l))))))
  6. L74
    specialize integer_span_pair_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (( · expand full local formula (737 characters)specialize integer_span_pair_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (l))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (k))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (j))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (i))))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (k))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (l))))))
  7. L75
    specialize integer_span_pair_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (( · expand full local formula (737 characters)specialize integer_span_pair_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (k))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (l))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (i))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (j))))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (l))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (k))))))
  8. L76
    apply integer_span_pair_equal_transitive
  9. L77
    exact hfirst_left
  10. L78
    exact hrotation_left
12Establish hrightL79–88

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply integer span pair equal transitive.

  1. L79
    have hright · expand full local formula (2,519 characters)have hright : ((((((((((((((d) * (e))) + (((c) * (f))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (i))) + (((((((((d) * (f))) + (((c) * (e))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (j))))) + (((((((((((((d) * (g))) + (((c) * (h))))) + (((((((a) + (d))) * (e))) + (((((b) + (c))) * (f))))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (l))) + (((((((((((d) * (h))) + (((c) * (g))))) + (((((((a) + (d))) * (f))) + (((((b) + (c))) * (e))))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (k))))))) + (((((((((a) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((b) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))))) + (((((c) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((d) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))))) + (((((c) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((d) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k)))))))))))))) = ((((((((((a) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((b) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))))) + (((((c) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((d) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))))) + (((((c) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((d) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))))))) + (((((((((((((d) * (e))) + (((c) * (f))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (j))) + (((((((((d) * (f))) + (((c) * (e))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (i))))) + (((((((((((((d) * (g))) + (((c) * (h))))) + (((((((a) + (d))) * (e))) + (((((b) + (c))) * (f))))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (k))) + (((((((((((d) * (h))) + (((c) * (g))))) + (((((((a) + (d))) * (f))) + (((((b) + (c))) * (e))))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (l))))))))
  2. L80
    specialize integer_span_pair_equal_transitive ((((((((((((d) * (e))) + (((c) * (f))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (i))) + (((((((((d) * (f))) + (((c) * (e))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (j))))) + (((((((((((((d) * (g))) + (((c) * (h))))) + (((((((a) + (d))) * (e))) + (((((b) + (c))) * (f))))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (l))) + (((((((((((d) * (h))) + (((c) * (g))))) + (((((((a) + (d))) * (f))) + (((((b) + (c))) * (e))))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (k))))))
  3. L81
    specialize integer_span_pair_equal_transitive ((((((((((((d) * (e))) + (((c) * (f))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (j))) + (((((((((d) * (f))) + (((c) * (e))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (i))))) + (((((((((((((d) * (g))) + (((c) * (h))))) + (((((((a) + (d))) * (e))) + (((((b) + (c))) * (f))))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (k))) + (((((((((((d) * (h))) + (((c) * (g))))) + (((((((a) + (d))) * (f))) + (((((b) + (c))) * (e))))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (l))))))
  4. L82
    specialize integer_span_pair_equal_transitive ((((((d) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((c) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))) + (((((((a) + (d))) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((((b) + (c))) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))))))
  5. L83
    specialize integer_span_pair_equal_transitive ((((((d) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((c) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))) + (((((((a) + (d))) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((((b) + (c))) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))))))
  6. L84
    specialize integer_span_pair_equal_transitive ((((((((a) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j · expand full local formula (737 characters)specialize integer_span_pair_equal_transitive ((((((((a) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((b) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))))) + (((((c) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((d) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))))) + (((((c) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((d) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))))))
  7. L85
    specialize integer_span_pair_equal_transitive ((((((((a) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i · expand full local formula (737 characters)specialize integer_span_pair_equal_transitive ((((((((a) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((b) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))))) + (((((c) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((d) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))))) + (((((c) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((d) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))))))
  8. L86
    apply integer_span_pair_equal_transitive
  9. L87
    specialize eisenstein_product_associate_real d
  10. L88
    specialize eisenstein_product_associate_real c
13Use earlier factsL89–98

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L89
    specialize eisenstein_product_associate_real ((a) + (d))
  2. L90
    specialize eisenstein_product_associate_real ((b) + (c))
  3. L91
    specialize eisenstein_product_associate_real e
  4. L92
    specialize eisenstein_product_associate_real f
  5. L93
    specialize eisenstein_product_associate_real g
  6. L94
    specialize eisenstein_product_associate_real h
  7. L95
    specialize eisenstein_product_associate_real i
  8. L96
    specialize eisenstein_product_associate_real j
  9. L97
    specialize eisenstein_product_associate_real k
  10. L98
    specialize eisenstein_product_associate_real l
14Use earlier factsL99–107

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L99
    apply eisenstein_product_associate_real
  2. L100
    exact hlast_left
  3. L101
    specialize integer_span_pair_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (( · expand full local formula (737 characters)specialize integer_span_pair_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (l))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (k))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (j))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (i))))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (k))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (l))))))
  4. L102
    specialize integer_span_pair_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (( · expand full local formula (737 characters)specialize integer_span_pair_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (k))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (l))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (i))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (j))))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (l))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (k))))))
  5. L103
    specialize integer_span_pair_equal_transitive ((((((((((((d) * (e))) + (((c) * (f))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (i))) + (((((((((d) * (f))) + (((c) * (e))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (j))))) + (((((((((((((d) * (g))) + (((c) * (h))))) + (((((((a) + (d))) * (e))) + (((((b) + (c))) * (f))))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (l))) + (((((((((((d) * (h))) + (((c) * (g))))) + (((((((a) + (d))) * (f))) + (((((b) + (c))) * (e))))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (k))))))
  6. L104
    specialize integer_span_pair_equal_transitive ((((((((((((d) * (e))) + (((c) * (f))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (j))) + (((((((((d) * (f))) + (((c) * (e))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (i))))) + (((((((((((((d) * (g))) + (((c) * (h))))) + (((((((a) + (d))) * (e))) + (((((b) + (c))) * (f))))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (k))) + (((((((((((d) * (h))) + (((c) * (g))))) + (((((((a) + (d))) * (f))) + (((((b) + (c))) * (e))))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (l))))))
  7. L105
    specialize integer_span_pair_equal_transitive ((((((((a) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j · expand full local formula (737 characters)specialize integer_span_pair_equal_transitive ((((((((a) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((b) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))))) + (((((c) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((d) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))))) + (((((c) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((d) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))))))
  8. L106
    specialize integer_span_pair_equal_transitive ((((((((a) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i · expand full local formula (737 characters)specialize integer_span_pair_equal_transitive ((((((((a) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((b) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))))) + (((((c) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((d) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))))) + (((((c) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((d) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))))))
  9. L107
    apply integer_span_pair_equal_transitive
15Calculate and transport equalitiesL108–108

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L108
    symm
16Use earlier factsL109–116

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L109
    exact hleft
  2. L110
    exact hright
  3. L111
    specialize matrix_integer_pair_negation_balance ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + · expand full local formula (739 characters)specialize matrix_integer_pair_negation_balance ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (l))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (k))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (j))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (i))))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (k))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (l))))))
  4. L112
    specialize matrix_integer_pair_negation_balance ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + · expand full local formula (739 characters)specialize matrix_integer_pair_negation_balance ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (k))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (l))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (i))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (j))))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (l))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (k))))))
  5. L113
    specialize matrix_integer_pair_negation_balance ((((((((a) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * · expand full local formula (739 characters)specialize matrix_integer_pair_negation_balance ((((((((a) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((b) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))))) + (((((c) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((d) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))))) + (((((c) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((d) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))))))
  6. L114
    specialize matrix_integer_pair_negation_balance ((((((((a) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * · expand full local formula (739 characters)specialize matrix_integer_pair_negation_balance ((((((((a) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((b) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))))) + (((((c) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((d) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))))) + (((((c) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((d) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))))))
  7. L115
    apply matrix_integer_pair_negation_balance
  8. L116
    exact hnegative

Library-wide reading audit

Original defined command ledger · 116 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro e
  6. 0006intro f
  7. 0007intro g
  8. 0008intro h
  9. 0009intro i
  10. 0010intro j
  11. 0011intro k
  12. 0012intro l
  13. 0013have hfirst : EisensteinCoordinateProduct(d · e + c · f + ((a + d) · h + (b + c) · g),d · f + c · e + ((a + d) · g + (b + c) · h),d · g + c · h + ((a + d) · e + (b + c) · f) + ((a + d) · h + (b + c) · g),d · h + c · g + ((a + d) · f + (b + c) · e) + ((a + d) · g + (b + c) · h),i,j,k,l,(a · h + b · g + (c · f + d · e) + (c · g + d · h)) · i + (a · g + b · h + (c · e + d · f) + (c · h + d · g)) · j + ((a · e + b · f + (c · h + d · g) + (a · h + b · g + (c · f + d · e) + (c · g + d · h))) · l + (a · f + b · e + (c · g + d · h) + (a · g + b · h + (c · e + d · f) + (c · h + d · g))) · k),(a · h + b · g + (c · f + d · e) + (c · g + d · h)) · j + (a · g + b · h + (c · e + d · f) + (c · h + d · g)) · i + ((a · e + b · f + (c · h + d · g) + (a · h + b · g + (c · f + d · e) + (c · g + d · h))) · k + (a · f + b · e + (c · g + d · h) + (a · g + b · h + (c · e + d · f) + (c · h + d · g))) · l),(a · h + b · g + (c · f + d · e) + (c · g + d · h)) · k + (a · g + b · h + (c · e + d · f) + (c · h + d · g)) · l + ((a · e + b · f + (c · h + d · g) + (a · h + b · g + (c · f + d · e) + (c · g + d · h))) · i + (a · f + b · e + (c · g + d · h) + (a · g + b · h + (c · e + d · f) + (c · h + d · g))) · j) + ((a · e + b · f + (c · h + d · g) + (a · h + b · g + (c · f + d · e) + (c · g + d · h))) · l + (a · f + b · e + (c · g + d · h) + (a · g + b · h + (c · e + d · f) + (c · h + d · g))) · k),(a · h + b · g + (c · f + d · e) + (c · g + d · h)) · l + (a · g + b · h + (c · e + d · f) + (c · h + d · g)) · k + ((a · e + b · f + (c · h + d · g) + (a · h + b · g + (c · f + d · e) + (c · g + d · h))) · j + (a · f + b · e + (c · g + d · h) + (a · g + b · h + (c · e + d · f) + (c · h + d · g))) · i) + ((a · e + b · f + (c · h + d · g) + (a · h + b · g + (c · f + d · e) + (c · g + d · h))) · k + (a · f + b · e + (c · g + d · h) + (a · g + b · h + (c · e + d · f) + (c · h + d · g))) · l))
  14. 0014specialize eisenstein_product_integer_congruence ((((((d) * (e))) + (((c) * (f))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))
  15. 0015specialize eisenstein_product_integer_congruence ((((((d) * (f))) + (((c) * (e))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))
  16. 0016specialize eisenstein_product_integer_congruence ((((((((d) * (g))) + (((c) * (h))))) + (((((((a) + (d))) * (e))) + (((((b) + (c))) * (f))))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))
  17. 0017specialize eisenstein_product_integer_congruence ((((((((d) * (h))) + (((c) * (g))))) + (((((((a) + (d))) * (f))) + (((((b) + (c))) * (e))))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))
  18. 0018specialize eisenstein_product_integer_congruence ((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))
  19. 0019specialize eisenstein_product_integer_congruence ((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))
  20. 0020specialize eisenstein_product_integer_congruence ((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))
  21. 0021specialize eisenstein_product_integer_congruence ((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))
  22. 0022specialize eisenstein_product_integer_congruence i
  23. 0023specialize eisenstein_product_integer_congruence j
  24. 0024specialize eisenstein_product_integer_congruence k
  25. 0025specialize eisenstein_product_integer_congruence l
  26. 0026specialize eisenstein_product_integer_congruence i
  27. 0027specialize eisenstein_product_integer_congruence j
  28. 0028specialize eisenstein_product_integer_congruence k
  29. 0029specialize eisenstein_product_integer_congruence l
  30. 0030apply eisenstein_product_integer_congruence
  31. 0031specialize eisenstein_omega_product_covariance a
  32. 0032specialize eisenstein_omega_product_covariance b
  33. 0033specialize eisenstein_omega_product_covariance c
  34. 0034specialize eisenstein_omega_product_covariance d
  35. 0035specialize eisenstein_omega_product_covariance e
  36. 0036specialize eisenstein_omega_product_covariance f
  37. 0037specialize eisenstein_omega_product_covariance g
  38. 0038specialize eisenstein_omega_product_covariance h
  39. 0039apply eisenstein_omega_product_covariance
  40. 0040specialize gaussian_equal_reflexive i
  41. 0041specialize gaussian_equal_reflexive j
  42. 0042specialize gaussian_equal_reflexive k
  43. 0043specialize gaussian_equal_reflexive l
  44. 0044apply gaussian_equal_reflexive
  45. 0045have hrotation : EisensteinCoordinateProduct(a · h + b · g + (c · f + d · e) + (c · g + d · h),a · g + b · h + (c · e + d · f) + (c · h + d · g),a · e + b · f + (c · h + d · g) + (a · h + b · g + (c · f + d · e) + (c · g + d · h)),a · f + b · e + (c · g + d · h) + (a · g + b · h + (c · e + d · f) + (c · h + d · g)),i,j,k,l,(a · e + b · f + (c · h + d · g)) · l + (a · f + b · e + (c · g + d · h)) · k + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · j + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · i) + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · k + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · l),(a · e + b · f + (c · h + d · g)) · k + (a · f + b · e + (c · g + d · h)) · l + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · i + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · j) + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · l + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · k),(a · e + b · f + (c · h + d · g)) · i + (a · f + b · e + (c · g + d · h)) · j + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · l + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · k) + ((a · e + b · f + (c · h + d · g)) · l + (a · f + b · e + (c · g + d · h)) · k + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · j + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · i) + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · k + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · l)),(a · e + b · f + (c · h + d · g)) · j + (a · f + b · e + (c · g + d · h)) · i + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · k + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · l) + ((a · e + b · f + (c · h + d · g)) · k + (a · f + b · e + (c · g + d · h)) · l + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · i + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · j) + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · l + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · k)))
  46. 0046specialize eisenstein_omega_product_covariance ((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))
  47. 0047specialize eisenstein_omega_product_covariance ((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))
  48. 0048specialize eisenstein_omega_product_covariance ((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))
  49. 0049specialize eisenstein_omega_product_covariance ((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))
  50. 0050specialize eisenstein_omega_product_covariance i
  51. 0051specialize eisenstein_omega_product_covariance j
  52. 0052specialize eisenstein_omega_product_covariance k
  53. 0053specialize eisenstein_omega_product_covariance l
  54. 0054apply eisenstein_omega_product_covariance
  55. 0055have hlast : EisensteinCoordinateProduct(d,c,a + d,b + c,e · i + f · j + (g · l + h · k),e · j + f · i + (g · k + h · l),e · k + f · l + (g · i + h · j) + (g · l + h · k),e · l + f · k + (g · j + h · i) + (g · k + h · l),a · (e · l + f · k + (g · j + h · i) + (g · k + h · l)) + b · (e · k + f · l + (g · i + h · j) + (g · l + h · k)) + (c · (e · j + f · i + (g · k + h · l)) + d · (e · i + f · j + (g · l + h · k))) + (c · (e · k + f · l + (g · i + h · j) + (g · l + h · k)) + d · (e · l + f · k + (g · j + h · i) + (g · k + h · l))),a · (e · k + f · l + (g · i + h · j) + (g · l + h · k)) + b · (e · l + f · k + (g · j + h · i) + (g · k + h · l)) + (c · (e · i + f · j + (g · l + h · k)) + d · (e · j + f · i + (g · k + h · l))) + (c · (e · l + f · k + (g · j + h · i) + (g · k + h · l)) + d · (e · k + f · l + (g · i + h · j) + (g · l + h · k))),a · (e · i + f · j + (g · l + h · k)) + b · (e · j + f · i + (g · k + h · l)) + (c · (e · l + f · k + (g · j + h · i) + (g · k + h · l)) + d · (e · k + f · l + (g · i + h · j) + (g · l + h · k))) + (a · (e · l + f · k + (g · j + h · i) + (g · k + h · l)) + b · (e · k + f · l + (g · i + h · j) + (g · l + h · k)) + (c · (e · j + f · i + (g · k + h · l)) + d · (e · i + f · j + (g · l + h · k))) + (c · (e · k + f · l + (g · i + h · j) + (g · l + h · k)) + d · (e · l + f · k + (g · j + h · i) + (g · k + h · l)))),a · (e · j + f · i + (g · k + h · l)) + b · (e · i + f · j + (g · l + h · k)) + (c · (e · k + f · l + (g · i + h · j) + (g · l + h · k)) + d · (e · l + f · k + (g · j + h · i) + (g · k + h · l))) + (a · (e · k + f · l + (g · i + h · j) + (g · l + h · k)) + b · (e · l + f · k + (g · j + h · i) + (g · k + h · l)) + (c · (e · i + f · j + (g · l + h · k)) + d · (e · j + f · i + (g · k + h · l))) + (c · (e · l + f · k + (g · j + h · i) + (g · k + h · l)) + d · (e · k + f · l + (g · i + h · j) + (g · l + h · k)))))
  56. 0056specialize eisenstein_omega_product_covariance a
  57. 0057specialize eisenstein_omega_product_covariance b
  58. 0058specialize eisenstein_omega_product_covariance c
  59. 0059specialize eisenstein_omega_product_covariance d
  60. 0060specialize eisenstein_omega_product_covariance ((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))
  61. 0061specialize eisenstein_omega_product_covariance ((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))
  62. 0062specialize eisenstein_omega_product_covariance ((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))
  63. 0063specialize eisenstein_omega_product_covariance ((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))
  64. 0064apply eisenstein_omega_product_covariance
  65. 0065cases hfirst
  66. 0066cases hrotation
  67. 0067cases hlast
  68. 0068have hnegative : ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (l))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (k))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (j))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (i))))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (k))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (l))))))) + (((((((((a) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((b) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))))) + (((((c) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((d) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))))) + (((((c) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((d) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k)))))))))))))) = ((((((((((a) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((b) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))))) + (((((c) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((d) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))))) + (((((c) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((d) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))))))) + (((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (k))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (l))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (i))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (j))))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (l))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (k))))))))
  69. 0069have hleft : ((((((((((((((d) * (e))) + (((c) * (f))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (i))) + (((((((((d) * (f))) + (((c) * (e))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (j))))) + (((((((((((((d) * (g))) + (((c) * (h))))) + (((((((a) + (d))) * (e))) + (((((b) + (c))) * (f))))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (l))) + (((((((((((d) * (h))) + (((c) * (g))))) + (((((((a) + (d))) * (f))) + (((((b) + (c))) * (e))))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (k))))))) + (((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (k))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (l))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (i))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (j))))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (l))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (k)))))))) = ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (l))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (k))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (j))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (i))))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (k))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (l))))))) + (((((((((((((d) * (e))) + (((c) * (f))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (j))) + (((((((((d) * (f))) + (((c) * (e))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (i))))) + (((((((((((((d) * (g))) + (((c) * (h))))) + (((((((a) + (d))) * (e))) + (((((b) + (c))) * (f))))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (k))) + (((((((((((d) * (h))) + (((c) * (g))))) + (((((((a) + (d))) * (f))) + (((((b) + (c))) * (e))))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (l))))))))
  70. 0070specialize integer_span_pair_equal_transitive ((((((((((((d) * (e))) + (((c) * (f))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (i))) + (((((((((d) * (f))) + (((c) * (e))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (j))))) + (((((((((((((d) * (g))) + (((c) * (h))))) + (((((((a) + (d))) * (e))) + (((((b) + (c))) * (f))))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (l))) + (((((((((((d) * (h))) + (((c) * (g))))) + (((((((a) + (d))) * (f))) + (((((b) + (c))) * (e))))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (k))))))
  71. 0071specialize integer_span_pair_equal_transitive ((((((((((((d) * (e))) + (((c) * (f))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (j))) + (((((((((d) * (f))) + (((c) * (e))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (i))))) + (((((((((((((d) * (g))) + (((c) * (h))))) + (((((((a) + (d))) * (e))) + (((((b) + (c))) * (f))))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (k))) + (((((((((((d) * (h))) + (((c) * (g))))) + (((((((a) + (d))) * (f))) + (((((b) + (c))) * (e))))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (l))))))
  72. 0072specialize integer_span_pair_equal_transitive ((((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (i))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (j))))) + (((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (l))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (k))))))
  73. 0073specialize integer_span_pair_equal_transitive ((((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (j))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (i))))) + (((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (k))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (l))))))
  74. 0074specialize integer_span_pair_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (l))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (k))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (j))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (i))))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (k))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (l))))))
  75. 0075specialize integer_span_pair_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (k))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (l))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (i))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (j))))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (l))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (k))))))
  76. 0076apply integer_span_pair_equal_transitive
  77. 0077exact hfirst_left
  78. 0078exact hrotation_left
  79. 0079have hright : ((((((((((((((d) * (e))) + (((c) * (f))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (i))) + (((((((((d) * (f))) + (((c) * (e))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (j))))) + (((((((((((((d) * (g))) + (((c) * (h))))) + (((((((a) + (d))) * (e))) + (((((b) + (c))) * (f))))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (l))) + (((((((((((d) * (h))) + (((c) * (g))))) + (((((((a) + (d))) * (f))) + (((((b) + (c))) * (e))))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (k))))))) + (((((((((a) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((b) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))))) + (((((c) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((d) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))))) + (((((c) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((d) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k)))))))))))))) = ((((((((((a) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((b) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))))) + (((((c) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((d) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))))) + (((((c) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((d) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))))))) + (((((((((((((d) * (e))) + (((c) * (f))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (j))) + (((((((((d) * (f))) + (((c) * (e))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (i))))) + (((((((((((((d) * (g))) + (((c) * (h))))) + (((((((a) + (d))) * (e))) + (((((b) + (c))) * (f))))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (k))) + (((((((((((d) * (h))) + (((c) * (g))))) + (((((((a) + (d))) * (f))) + (((((b) + (c))) * (e))))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (l))))))))
  80. 0080specialize integer_span_pair_equal_transitive ((((((((((((d) * (e))) + (((c) * (f))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (i))) + (((((((((d) * (f))) + (((c) * (e))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (j))))) + (((((((((((((d) * (g))) + (((c) * (h))))) + (((((((a) + (d))) * (e))) + (((((b) + (c))) * (f))))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (l))) + (((((((((((d) * (h))) + (((c) * (g))))) + (((((((a) + (d))) * (f))) + (((((b) + (c))) * (e))))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (k))))))
  81. 0081specialize integer_span_pair_equal_transitive ((((((((((((d) * (e))) + (((c) * (f))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (j))) + (((((((((d) * (f))) + (((c) * (e))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (i))))) + (((((((((((((d) * (g))) + (((c) * (h))))) + (((((((a) + (d))) * (e))) + (((((b) + (c))) * (f))))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (k))) + (((((((((((d) * (h))) + (((c) * (g))))) + (((((((a) + (d))) * (f))) + (((((b) + (c))) * (e))))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (l))))))
  82. 0082specialize integer_span_pair_equal_transitive ((((((d) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((c) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))) + (((((((a) + (d))) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((((b) + (c))) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))))))
  83. 0083specialize integer_span_pair_equal_transitive ((((((d) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((c) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))) + (((((((a) + (d))) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((((b) + (c))) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))))))
  84. 0084specialize integer_span_pair_equal_transitive ((((((((a) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((b) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))))) + (((((c) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((d) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))))) + (((((c) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((d) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))))))
  85. 0085specialize integer_span_pair_equal_transitive ((((((((a) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((b) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))))) + (((((c) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((d) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))))) + (((((c) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((d) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))))))
  86. 0086apply integer_span_pair_equal_transitive
  87. 0087specialize eisenstein_product_associate_real d
  88. 0088specialize eisenstein_product_associate_real c
  89. 0089specialize eisenstein_product_associate_real ((a) + (d))
  90. 0090specialize eisenstein_product_associate_real ((b) + (c))
  91. 0091specialize eisenstein_product_associate_real e
  92. 0092specialize eisenstein_product_associate_real f
  93. 0093specialize eisenstein_product_associate_real g
  94. 0094specialize eisenstein_product_associate_real h
  95. 0095specialize eisenstein_product_associate_real i
  96. 0096specialize eisenstein_product_associate_real j
  97. 0097specialize eisenstein_product_associate_real k
  98. 0098specialize eisenstein_product_associate_real l
  99. 0099apply eisenstein_product_associate_real
  100. 0100exact hlast_left
  101. 0101specialize integer_span_pair_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (l))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (k))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (j))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (i))))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (k))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (l))))))
  102. 0102specialize integer_span_pair_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (k))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (l))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (i))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (j))))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (l))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (k))))))
  103. 0103specialize integer_span_pair_equal_transitive ((((((((((((d) * (e))) + (((c) * (f))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (i))) + (((((((((d) * (f))) + (((c) * (e))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (j))))) + (((((((((((((d) * (g))) + (((c) * (h))))) + (((((((a) + (d))) * (e))) + (((((b) + (c))) * (f))))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (l))) + (((((((((((d) * (h))) + (((c) * (g))))) + (((((((a) + (d))) * (f))) + (((((b) + (c))) * (e))))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (k))))))
  104. 0104specialize integer_span_pair_equal_transitive ((((((((((((d) * (e))) + (((c) * (f))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (j))) + (((((((((d) * (f))) + (((c) * (e))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (i))))) + (((((((((((((d) * (g))) + (((c) * (h))))) + (((((((a) + (d))) * (e))) + (((((b) + (c))) * (f))))))) + (((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))))) * (k))) + (((((((((((d) * (h))) + (((c) * (g))))) + (((((((a) + (d))) * (f))) + (((((b) + (c))) * (e))))))) + (((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))))) * (l))))))
  105. 0105specialize integer_span_pair_equal_transitive ((((((((a) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((b) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))))) + (((((c) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((d) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))))) + (((((c) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((d) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))))))
  106. 0106specialize integer_span_pair_equal_transitive ((((((((a) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((b) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))))) + (((((c) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((d) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))))) + (((((c) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((d) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))))))
  107. 0107apply integer_span_pair_equal_transitive
  108. 0108symm
  109. 0109exact hleft
  110. 0110exact hright
  111. 0111specialize matrix_integer_pair_negation_balance ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (l))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (k))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (j))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (i))))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (k))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (l))))))
  112. 0112specialize matrix_integer_pair_negation_balance ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (k))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (l))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (i))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (j))))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (l))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (k))))))
  113. 0113specialize matrix_integer_pair_negation_balance ((((((((a) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((b) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))))) + (((((c) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((d) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))))) + (((((c) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((d) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))))))
  114. 0114specialize matrix_integer_pair_negation_balance ((((((((a) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((b) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))))) + (((((c) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((d) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))))) + (((((c) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((d) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))))))
  115. 0115apply matrix_integer_pair_negation_balance
  116. 0116exact hnegative