Skip to content

Commit

Permalink
Merge pull request #85 from hcsch/algo-l7-typo-fix
Browse files Browse the repository at this point in the history
Fix typo in `contrapose! h` explainer in algorithm world level 7
  • Loading branch information
kbuzzard authored Feb 1, 2025
2 parents d72628a + 47e9945 commit 06961e0
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Game/Levels/Algorithm/L07succ_ne_succ.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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!)"
Expand Down

0 comments on commit 06961e0

Please sign in to comment.