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