greg/NNG
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Merge pull request #85 from hcsch/algo-l7-typo-fix

Browse Source 
Fix typo in `contrapose! h` explainer in algorithm world level 7
This commit is contained in:
Kevin Buzzard
2025-02-01 23:01:23 +00:00
committed by GitHub
parent d72628a80c 47e9945ff9
commit 06961e07eb
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
Game/Levels/Algorithm/L07succ_ne_succ.lean
View File

@@ -60,7 +60,7 @@ TheoremDoc MyNat.succ_ne_succ as "succ_ne_succ" in "Peano"
/-- If $a \neq b$ then $\operatorname{succ}(a) \neq\operatorname{succ}(b)$. -/
Statement succ_ne_succ (m n : ℕ) (h : m ≠ n) : succ m ≠ succ n := by
Hint "Start with `contrapose! h`, to change the goal into its
contrapositive, namely a hypothesis of `succ m = succ m` and a goal of `m = n`."
contrapositive, namely a hypothesis of `succ m = succ n` and a goal of `m = n`."
contrapose! h
Hint "Can you take it from here? (note: if you try `contrapose! h` again, it will
take you back to where you started!)"