Merge pull request #33 from jonasspinner/patch-1

Small fix for L03add_left_cancel
2023-10-24 21:38:09 +02:00
parent 4d7a1c99c1 0f5bc451a9
commit 99e1017361
1 changed files with 1 additions and 1 deletions
--- a/Game/Levels/AdvAddition/L03add_left_cancel.lean
+++ b/Game/Levels/AdvAddition/L03add_left_cancel.lean
@@ -18,7 +18,7 @@ Introduction
 You can prove it by induction on `n` or you can deduce it from `add_right_cancel`.
 "

-/-- $a+n=b+n\implies a=b$. -/
+/-- $n+a=n+b\implies a=b$. -/
 Statement add_left_cancel (a b n : ℕ) : n + a = n + b → a = b := by
  repeat rw [add_comm n]
  intro h