Generated central-inversion checks, group 1.

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor19 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 19) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 19)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid19 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 19) : witness.Valid 19

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor20 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 20) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 20)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid20 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 20) : witness.Valid 20

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor21 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 21) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 21)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid21 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 21) : witness.Valid 21

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor22 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 22) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 22)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid22 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 22) : witness.Valid 22

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor23 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 23) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 23)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid23 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 23) : witness.Valid 23

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor24 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 24) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 24)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid24 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 24) : witness.Valid 24

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor25 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 25) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 25)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid25 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 25) : witness.Valid 25

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor26 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 26) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 26)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid26 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 26) : witness.Valid 26

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor27 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 27) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 27)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid27 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 27) : witness.Valid 27

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor28 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 28) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 28)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid28 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 28) : witness.Valid 28

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor29 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 29) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 29)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid29 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 29) : witness.Valid 29

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor30 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 30) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 30)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid30 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 30) : witness.Valid 30

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor31 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 31) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 31)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid31 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 31) : witness.Valid 31

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor32 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 32) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 32)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid32 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 32) : witness.Valid 32

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor33 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 33) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 33)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid33 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 33) : witness.Valid 33

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor34 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 34) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 34)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid34 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 34) : witness.Valid 34

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor35 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 35) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 35)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid35 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 35) : witness.Valid 35

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor36 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 36) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 36)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid36 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 36) : witness.Valid 36

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor37 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 37) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 37)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid37 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 37) : witness.Valid 37