diff --git a/PrimeNumberTheoremAnd/SecondProofPNT.lean b/PrimeNumberTheoremAnd/SecondProofPNT.lean
index 15411d4b..41342e0a 100644
--- a/PrimeNumberTheoremAnd/SecondProofPNT.lean
+++ b/PrimeNumberTheoremAnd/SecondProofPNT.lean
@@ -126,6 +126,7 @@ For any $T>0$, there is a $\delta>0$ so that $[1-\delta,1] \times_{ℂ} [-T,T]$
 
 /-%%
 \begin{proof}
+\uses{NoZerosInBoxOfNoneOnBoundary}
 We have that zeta doesn't vanish on the 1 line and is holomorphic inside the box (except for the pole at $s=1$). If for a height $T>0$, there was no such $\delta$, then there would be a sequence of zeros of $\zeta$ approaching the 1 line, and by compactness, we could find a subsequence of zeros converging to a point on the 1 line. But then $\zeta$ would vanish at that point, a contradiction. (Worse yet, zeta would then be entirely zero...)
 \end{proof}
 %%-/
@@ -159,7 +160,7 @@ X^{s}ds = \frac{X^{1}}{1}\mathcal{M}(\widetilde{1_{\epsilon}})(1)
 
 /-%%
 \begin{proof}
-\uses{ZeroFreeBox, RectangleIntegral, ResidueOfLogDerivative, MellinOfSmooth1, MellinOfDeltaSpikeAt1}
+\uses{ZeroFreeBox, Rectangle, RectangleBorder, RectangleIntegral, ResidueOfLogDerivative, MellinOfSmooth1, MellinOfDeltaSpikeAt1}
 Residue calculus / the argument principle.
 \end{proof}
 %%-/
@@ -179,3 +180,17 @@ where:
 \end{itemize}
 
 %%-/
+/-%%
+\section{Weak PNT'}
+
+\begin{theorem}[Weak PNT']\label{WeakPNT'}  We have
+$$ \sum_{n \leq x} \Lambda(n) = x + o(x).$$
+\end{theorem}
+%%-/
+
+/-%%
+\begin{proof}
+\uses{ChebyshevPsi, SmoothedChebyshevClose, ZetaBoxEval}
+  Evaluate the integrals.
+\end{proof}
+%%-/
diff --git a/PrimeNumberTheoremAnd/StrongPNT.lean b/PrimeNumberTheoremAnd/StrongPNT.lean
index 11627be4..bf5fe75b 100644
--- a/PrimeNumberTheoremAnd/StrongPNT.lean
+++ b/PrimeNumberTheoremAnd/StrongPNT.lean
@@ -23,7 +23,7 @@ noncomputable def ChebyshevPsi (x : ℝ) : ℝ := (Finset.range (Nat.floor x)).s
 /-%%
 
 Main Theorem: The Prime Number Theorem in strong form.
-\begin{theorem}[PrimeNumberTheorem]\label{StrongPNT}\lean{PrimeNumberTheorem}\uses{WienerIkehara}
+\begin{theorem}[PrimeNumberTheorem]\label{StrongPNT}\lean{PrimeNumberTheorem}\uses{WienerIkehara, ChebysevPsi}
 There is a constant $c > 0$ such that
 $$
 ψ (x) = x + O(x e^{-c \sqrt{\log x}})