LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock5Vars12to15

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.siIntGoal_block5_var12 (p q : Fin 3) : SiIntGoal ⟨5, ⋯⟩ ⟨12, ⋯⟩ p q

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.siIntGoal_block5_var13 (p q : Fin 3) : SiIntGoal ⟨5, ⋯⟩ ⟨13, ⋯⟩ p q

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.siIntGoal_block5_var14 (p q : Fin 3) : SiIntGoal ⟨5, ⋯⟩ ⟨14, ⋯⟩ p q

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.siIntGoal_block5_var15 (p q : Fin 3) : SiIntGoal ⟨5, ⋯⟩ ⟨15, ⋯⟩ p q