LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock5Vars4to7

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.siIntGoal_block5_var4 (p q : Fin 3) : SiIntGoal ⟨5, siIntGoal_block5_var4._proof_1⟩ ⟨4, siIntGoal_block5_var4._proof_2⟩ p q

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.siIntGoal_block5_var5 (p q : Fin 3) : SiIntGoal ⟨5, siIntGoal_block5_var4._proof_1⟩ ⟨5, siIntGoal_block5_var5._proof_1⟩ p q

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.siIntGoal_block5_var6 (p q : Fin 3) : SiIntGoal ⟨5, siIntGoal_block5_var4._proof_1⟩ ⟨6, siIntGoal_block5_var6._proof_1⟩ p q

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.siIntGoal_block5_var7 (p q : Fin 3) : SiIntGoal ⟨5, siIntGoal_block5_var4._proof_1⟩ ⟨7, siIntGoal_block5_var7._proof_1⟩ p q