LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock1Vars12to15

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.siIntGoal_block1_var12 (p q : Fin 3) : SiIntGoal ⟨1, siIntGoal_block1_var12._proof_1⟩ ⟨12, siIntGoal_block1_var12._proof_2⟩ p q

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.siIntGoal_block1_var13 (p q : Fin 3) : SiIntGoal ⟨1, siIntGoal_block1_var12._proof_1⟩ ⟨13, siIntGoal_block1_var13._proof_1⟩ p q

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.siIntGoal_block1_var14 (p q : Fin 3) : SiIntGoal ⟨1, siIntGoal_block1_var12._proof_1⟩ ⟨14, siIntGoal_block1_var14._proof_1⟩ p q

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.siIntGoal_block1_var15 (p q : Fin 3) : SiIntGoal ⟨1, siIntGoal_block1_var12._proof_1⟩ ⟨15, siIntGoal_block1_var15._proof_1⟩ p q