Merge pull request #29 from Madjosz/patch-1

Fix L07intro2.lean conclusion
leanprover-community · Oct 17, 2023 · 4631fa2 · 4631fa2
2 parents 75bb4e5 + ef2c861
commit 4631fa2
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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
 ```
 "