Generated central-inversion checks, group 3.

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor57 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 57) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 57)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid57 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 57) : witness.Valid 57

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor58 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 58) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 58)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid58 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 58) : witness.Valid 58

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor59 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 59) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 59)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid59 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 59) : witness.Valid 59

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor60 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 60) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 60)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid60 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 60) : witness.Valid 60

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor61 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 61) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 61)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid61 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 61) : witness.Valid 61

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor62 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 62) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 62)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid62 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 62) : witness.Valid 62

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor63 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 63) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 63)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid63 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 63) : witness.Valid 63

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor64 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 64) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 64)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid64 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 64) : witness.Valid 64

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor65 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 65) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 65)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid65 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 65) : witness.Valid 65

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor66 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 66) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 66)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid66 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 66) : witness.Valid 66

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor67 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 67) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 67)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid67 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 67) : witness.Valid 67

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor68 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 68) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 68)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid68 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 68) : witness.Valid 68

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor69 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 69) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 69)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid69 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 69) : witness.Valid 69

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor70 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 70) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 70)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid70 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 70) : witness.Valid 70

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor71 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 71) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 71)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid71 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 71) : witness.Valid 71

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor72 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 72) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 72)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid72 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 72) : witness.Valid 72