Generated central-inversion checks, group 2.

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor38 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 38) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 38)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid38 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 38) : witness.Valid 38

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor39 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 39) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 39)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid39 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 39) : witness.Valid 39

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor40 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 40) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 40)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid40 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 40) : witness.Valid 40

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor41 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 41) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 41)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid41 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 41) : witness.Valid 41

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor42 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 42) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 42)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid42 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 42) : witness.Valid 42

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor43 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 43) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 43)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid43 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 43) : witness.Valid 43

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor44 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 44) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 44)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid44 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 44) : witness.Valid 44

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor45 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 45) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 45)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid45 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 45) : witness.Valid 45

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor46 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 46) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 46)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid46 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 46) : witness.Valid 46

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor47 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 47) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 47)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid47 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 47) : witness.Valid 47

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor48 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 48) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 48)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid48 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 48) : witness.Valid 48

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor49 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 49) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 49)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid49 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 49) : witness.Valid 49

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor50 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 50) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 50)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid50 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 50) : witness.Valid 50

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor51 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 51) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 51)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid51 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 51) : witness.Valid 51

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor52 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 52) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 52)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid52 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 52) : witness.Valid 52

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor53 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 53) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 53)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid53 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 53) : witness.Valid 53

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor54 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 54) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 54)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid54 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 54) : witness.Valid 54

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor55 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 55) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 55)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid55 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 55) : witness.Valid 55

theorem HadwigerNelsonBounds.partsGadgetNegationNeighbor56 {neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors 56) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation 56)

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

theorem HadwigerNelsonBounds.partsGadgetTriangleWitnessValid56 {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses 56) : witness.Valid 56