LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock4Vars16to19

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

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.siIntGoal_block4_var17 (p q : Fin 3) : SiIntGoal ⟨4, siIntGoal_block4_var16._proof_1⟩ ⟨17, siIntGoal_block4_var17._proof_1⟩ p q

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.siIntGoal_block4_var18 (p q : Fin 3) : SiIntGoal ⟨4, siIntGoal_block4_var16._proof_1⟩ ⟨18, siIntGoal_block4_var18._proof_1⟩ p q

theorem Distributed2Coloring.LowerBound.N1000000BCompressionCompute.siIntGoal_block4_var19 (p q : Fin 3) : SiIntGoal ⟨4, siIntGoal_block4_var16._proof_1⟩ ⟨19, siIntGoal_block4_var19._proof_1⟩ p q