Generated central-inversion checks, group 0.

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor0 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 0) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 0)

theorem HadwigerNelsonBounds.partsGadgetNegationTriple0 {pair : Fin 73 × Fin 73} (hpair : pair ∈ partsGadgetTriplePairs 0) : (partsGadgetNegation pair.1, partsGadgetNegation pair.2) ∈ partsGadgetTriplePairs (partsGadgetNegation 0) ∨ (partsGadgetNegation pair.2, partsGadgetNegation pair.1) ∈ partsGadgetTriplePairs (partsGadgetNegation 0)

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid0 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 0) : witness.Valid 0

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor1 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 1) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 1)

theorem HadwigerNelsonBounds.partsGadgetNegationTriple1 {pair : Fin 73 × Fin 73} (hpair : pair ∈ partsGadgetTriplePairs 1) : (partsGadgetNegation pair.1, partsGadgetNegation pair.2) ∈ partsGadgetTriplePairs (partsGadgetNegation 1) ∨ (partsGadgetNegation pair.2, partsGadgetNegation pair.1) ∈ partsGadgetTriplePairs (partsGadgetNegation 1)

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid1 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 1) : witness.Valid 1

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor2 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 2) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 2)

theorem HadwigerNelsonBounds.partsGadgetNegationTriple2 {pair : Fin 73 × Fin 73} (hpair : pair ∈ partsGadgetTriplePairs 2) : (partsGadgetNegation pair.1, partsGadgetNegation pair.2) ∈ partsGadgetTriplePairs (partsGadgetNegation 2) ∨ (partsGadgetNegation pair.2, partsGadgetNegation pair.1) ∈ partsGadgetTriplePairs (partsGadgetNegation 2)

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid2 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 2) : witness.Valid 2

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor3 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 3) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 3)

theorem HadwigerNelsonBounds.partsGadgetNegationTriple3 {pair : Fin 73 × Fin 73} (hpair : pair ∈ partsGadgetTriplePairs 3) : (partsGadgetNegation pair.1, partsGadgetNegation pair.2) ∈ partsGadgetTriplePairs (partsGadgetNegation 3) ∨ (partsGadgetNegation pair.2, partsGadgetNegation pair.1) ∈ partsGadgetTriplePairs (partsGadgetNegation 3)

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid3 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 3) : witness.Valid 3

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor4 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 4) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 4)

theorem HadwigerNelsonBounds.partsGadgetNegationTriple4 {pair : Fin 73 × Fin 73} (hpair : pair ∈ partsGadgetTriplePairs 4) : (partsGadgetNegation pair.1, partsGadgetNegation pair.2) ∈ partsGadgetTriplePairs (partsGadgetNegation 4) ∨ (partsGadgetNegation pair.2, partsGadgetNegation pair.1) ∈ partsGadgetTriplePairs (partsGadgetNegation 4)

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid4 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 4) : witness.Valid 4

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor5 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 5) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 5)

theorem HadwigerNelsonBounds.partsGadgetNegationTriple5 {pair : Fin 73 × Fin 73} (hpair : pair ∈ partsGadgetTriplePairs 5) : (partsGadgetNegation pair.1, partsGadgetNegation pair.2) ∈ partsGadgetTriplePairs (partsGadgetNegation 5) ∨ (partsGadgetNegation pair.2, partsGadgetNegation pair.1) ∈ partsGadgetTriplePairs (partsGadgetNegation 5)

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid5 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 5) : witness.Valid 5

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor6 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 6) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 6)

theorem HadwigerNelsonBounds.partsGadgetNegationTriple6 {pair : Fin 73 × Fin 73} (hpair : pair ∈ partsGadgetTriplePairs 6) : (partsGadgetNegation pair.1, partsGadgetNegation pair.2) ∈ partsGadgetTriplePairs (partsGadgetNegation 6) ∨ (partsGadgetNegation pair.2, partsGadgetNegation pair.1) ∈ partsGadgetTriplePairs (partsGadgetNegation 6)

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid6 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 6) : witness.Valid 6

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor7 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 7) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 7)

theorem HadwigerNelsonBounds.partsGadgetNegationTriple7 {pair : Fin 73 × Fin 73} (hpair : pair ∈ partsGadgetTriplePairs 7) : (partsGadgetNegation pair.1, partsGadgetNegation pair.2) ∈ partsGadgetTriplePairs (partsGadgetNegation 7) ∨ (partsGadgetNegation pair.2, partsGadgetNegation pair.1) ∈ partsGadgetTriplePairs (partsGadgetNegation 7)

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid7 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 7) : witness.Valid 7

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor8 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 8) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 8)

theorem HadwigerNelsonBounds.partsGadgetNegationTriple8 {pair : Fin 73 × Fin 73} (hpair : pair ∈ partsGadgetTriplePairs 8) : (partsGadgetNegation pair.1, partsGadgetNegation pair.2) ∈ partsGadgetTriplePairs (partsGadgetNegation 8) ∨ (partsGadgetNegation pair.2, partsGadgetNegation pair.1) ∈ partsGadgetTriplePairs (partsGadgetNegation 8)

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid8 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 8) : witness.Valid 8

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor9 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 9) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 9)

theorem HadwigerNelsonBounds.partsGadgetNegationTriple9 {pair : Fin 73 × Fin 73} (hpair : pair ∈ partsGadgetTriplePairs 9) : (partsGadgetNegation pair.1, partsGadgetNegation pair.2) ∈ partsGadgetTriplePairs (partsGadgetNegation 9) ∨ (partsGadgetNegation pair.2, partsGadgetNegation pair.1) ∈ partsGadgetTriplePairs (partsGadgetNegation 9)

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid9 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 9) : witness.Valid 9

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor10 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 10) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 10)

theorem HadwigerNelsonBounds.partsGadgetNegationTriple10 {pair : Fin 73 × Fin 73} (hpair : pair ∈ partsGadgetTriplePairs 10) : (partsGadgetNegation pair.1, partsGadgetNegation pair.2) ∈ partsGadgetTriplePairs (partsGadgetNegation 10) ∨ (partsGadgetNegation pair.2, partsGadgetNegation pair.1) ∈ partsGadgetTriplePairs (partsGadgetNegation 10)

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid10 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 10) : witness.Valid 10

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor11 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 11) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 11)

theorem HadwigerNelsonBounds.partsGadgetNegationTriple11 {pair : Fin 73 × Fin 73} (hpair : pair ∈ partsGadgetTriplePairs 11) : (partsGadgetNegation pair.1, partsGadgetNegation pair.2) ∈ partsGadgetTriplePairs (partsGadgetNegation 11) ∨ (partsGadgetNegation pair.2, partsGadgetNegation pair.1) ∈ partsGadgetTriplePairs (partsGadgetNegation 11)

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid11 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 11) : witness.Valid 11

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor12 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 12) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 12)

theorem HadwigerNelsonBounds.partsGadgetNegationTriple12 {pair : Fin 73 × Fin 73} (hpair : pair ∈ partsGadgetTriplePairs 12) : (partsGadgetNegation pair.1, partsGadgetNegation pair.2) ∈ partsGadgetTriplePairs (partsGadgetNegation 12) ∨ (partsGadgetNegation pair.2, partsGadgetNegation pair.1) ∈ partsGadgetTriplePairs (partsGadgetNegation 12)

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid12 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 12) : witness.Valid 12

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor13 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 13) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 13)

theorem HadwigerNelsonBounds.partsGadgetNegationTriple13 {pair : Fin 73 × Fin 73} (hpair : pair ∈ partsGadgetTriplePairs 13) : (partsGadgetNegation pair.1, partsGadgetNegation pair.2) ∈ partsGadgetTriplePairs (partsGadgetNegation 13) ∨ (partsGadgetNegation pair.2, partsGadgetNegation pair.1) ∈ partsGadgetTriplePairs (partsGadgetNegation 13)

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid13 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 13) : witness.Valid 13

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor14 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 14) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 14)

theorem HadwigerNelsonBounds.partsGadgetNegationTriple14 {pair : Fin 73 × Fin 73} (hpair : pair ∈ partsGadgetTriplePairs 14) : (partsGadgetNegation pair.1, partsGadgetNegation pair.2) ∈ partsGadgetTriplePairs (partsGadgetNegation 14) ∨ (partsGadgetNegation pair.2, partsGadgetNegation pair.1) ∈ partsGadgetTriplePairs (partsGadgetNegation 14)

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid14 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 14) : witness.Valid 14

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor15 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 15) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 15)

theorem HadwigerNelsonBounds.partsGadgetNegationTriple15 {pair : Fin 73 × Fin 73} (hpair : pair ∈ partsGadgetTriplePairs 15) : (partsGadgetNegation pair.1, partsGadgetNegation pair.2) ∈ partsGadgetTriplePairs (partsGadgetNegation 15) ∨ (partsGadgetNegation pair.2, partsGadgetNegation pair.1) ∈ partsGadgetTriplePairs (partsGadgetNegation 15)

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid15 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 15) : witness.Valid 15

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor16 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 16) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 16)

theorem HadwigerNelsonBounds.partsGadgetNegationTriple16 {pair : Fin 73 × Fin 73} (hpair : pair ∈ partsGadgetTriplePairs 16) : (partsGadgetNegation pair.1, partsGadgetNegation pair.2) ∈ partsGadgetTriplePairs (partsGadgetNegation 16) ∨ (partsGadgetNegation pair.2, partsGadgetNegation pair.1) ∈ partsGadgetTriplePairs (partsGadgetNegation 16)

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid16 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 16) : witness.Valid 16

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor17 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 17) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 17)

theorem HadwigerNelsonBounds.partsGadgetNegationTriple17 {pair : Fin 73 × Fin 73} (hpair : pair ∈ partsGadgetTriplePairs 17) : (partsGadgetNegation pair.1, partsGadgetNegation pair.2) ∈ partsGadgetTriplePairs (partsGadgetNegation 17) ∨ (partsGadgetNegation pair.2, partsGadgetNegation pair.1) ∈ partsGadgetTriplePairs (partsGadgetNegation 17)

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid17 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 17) : witness.Valid 17

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor18 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 18) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 18)

theorem HadwigerNelsonBounds.partsGadgetNegationTriple18 {pair : Fin 73 × Fin 73} (hpair : pair ∈ partsGadgetTriplePairs 18) : (partsGadgetNegation pair.1, partsGadgetNegation pair.2) ∈ partsGadgetTriplePairs (partsGadgetNegation 18) ∨ (partsGadgetNegation pair.2, partsGadgetNegation pair.1) ∈ partsGadgetTriplePairs (partsGadgetNegation 18)

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid18 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 18) : witness.Valid 18