diff --git a/Game/MyNat/Addition.lean b/Game/MyNat/Addition.lean
index ae314ef..9cd4b23 100644
--- a/Game/MyNat/Addition.lean
+++ b/Game/MyNat/Addition.lean
@@ -22,9 +22,3 @@ If `a` and `d` are natural numbers, then `add_succ a d` is the proof that
 -/
 @[MyNat_decide]
 axiom add_succ (a d : MyNat) : a + (succ d) = succ (a + d)
-
--- -- don't tell the viewers, we cheat with decide because
--- -- we used axioms to define nat
--- @[MyNat_decide]
--- theorem toNat_add (m n : MyNat) : (m + n).toNat = m.toNat + n.toNat := by
---   induction n <;> simp [MyNat_decide, Nat.add_succ, *];