From 0934f6265f16c7845c61fc00142153448e443825 Mon Sep 17 00:00:00 2001
From: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Date: Sun, 17 Mar 2024 22:46:13 +0000
Subject: [PATCH] this should disable zero-ne-succ

---
 Game/Levels/Algorithm/L06is_zero.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Game/Levels/Algorithm/L06is_zero.lean b/Game/Levels/Algorithm/L06is_zero.lean
index 9d1ce8f..7f6f5f8 100644
--- a/Game/Levels/Algorithm/L06is_zero.lean
+++ b/Game/Levels/Algorithm/L06is_zero.lean
@@ -61,3 +61,5 @@ Statement succ_ne_zero (a : ℕ) : succ a ≠ 0 := by
   rw [h]
   rw [is_zero_zero]
   triv
+
+DisabledTheorem MyNat.zero_ne_succ