diff --git a/formal/SilverSight/BlockCoprimeDensity.lean b/formal/SilverSight/BlockCoprimeDensity.lean
index 768d37e1..3d53e8ba 100644
--- a/formal/SilverSight/BlockCoprimeDensity.lean
+++ b/formal/SilverSight/BlockCoprimeDensity.lean
@@ -227,7 +227,6 @@ lemma D_finite_zero_eq (G : ℕ) : D_finite 0 G = Finset.prod (primesUpTo G) (fu
   have h : ∀ p ∈ primesUpTo G, (1 - (1 : ℚ) / ((p : ℚ) ^ 2))⁻¹ * (1 - (1 : ℚ) / ((p : ℚ) ^ 2)) = 1 := by
     intro p hp
     have hp_prime : Nat.Prime p := (Finset.mem_filter.mp hp).2
-    have hp_sq_ne_zero : (p : ℚ) ^ 2 ≠ 0 := pow_ne_zero 2 (by exact_mod_cast (Nat.Prime.ne_zero hp_prime))
     have hx : (1 - (1 : ℚ) / ((p : ℚ) ^ 2)) ≠ 0 := by
       have hp_gt_one : (p : ℚ) > 1 := by exact_mod_cast (Nat.Prime.one_lt hp_prime)
       have hp_sq_gt_one : (p : ℚ) ^ 2 > 1 := by nlinarith