LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock5Vars8to11

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

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

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

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