LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock2Vars12to15

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

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

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

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