diff --git a/content/blog/lean4-tutorial.md b/content/blog/lean4-tutorial.md
index 8cd2de9..cb3ec57 100644
--- a/content/blog/lean4-tutorial.md
+++ b/content/blog/lean4-tutorial.md
@@ -215,7 +215,7 @@ example {p q : Prop} (H_pq : p → q) (H_pnq : p → ¬q) : ¬p := by
   exact show False from H_nq H_q
 ```
 
-### Negation Elimination
+### Double Negation Elimination
 
 One common representation of negation elimination is to remove any double negations.
 That is $\neg \neg P$ becomes $P$.
@@ -261,6 +261,8 @@ example {p: Prop} (H_nnp : ¬¬p) : p := by
     exact show p from False.elim H_false
 ```
 
+Lean has this theorem built-in with `Classical.not_not`.
+
 ## First Order
 
 Lean is also capable of reasoning over first order logic. In this section, we'll start seeing objects/terms and predicates instead of just propositions.
@@ -498,3 +500,6 @@ inductions as writing out the cases explicitly can be daunting.
 
 If you catch any mistakes in me converting this post, let me know.
 Otherwise feel free to email me if you have any questions.
+
+Lastly, I want to give my thanks to James Oswald for helping proofread
+this post and making it better.