LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock4

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.siIntGoal_block4 (i : Var) (p q : Fin 3) : SiIntGoal ⟨4, ⋯⟩ i p q