From ef2c8616d42c399d916bd17f9e913321d083d527 Mon Sep 17 00:00:00 2001
From: Madjosz <28844868+Madjosz@users.noreply.github.com>
Date: Mon, 16 Oct 2023 20:17:33 +0200
Subject: [PATCH] Fix L07intro2.lean conclusion

---
 Game/Levels/Implication/L07intro2.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Game/Levels/Implication/L07intro2.lean b/Game/Levels/Implication/L07intro2.lean
index 842374d..d02f76c 100644
--- a/Game/Levels/Implication/L07intro2.lean
+++ b/Game/Levels/Implication/L07intro2.lean
@@ -26,8 +26,8 @@ Statement (x : ℕ) : x + 1 = y + 1 → x = y := by
 Conclusion "Here's a completely backwards proof:
 ```
 intro h
-repeat rw [succ_eq_add_one]
 apply succ_inj
+repeat rw [succ_eq_add_one]
 exact h
 ```
 "