doc: add conclusion for adv multn L8

2025-02-17 10:09:59 +00:00
parent a59282f10b
commit 36a82b7cfd
1 changed files with 9 additions and 0 deletions
--- a/Game/Levels/AdvMultiplication/L08mul_eq_zero.lean
+++ b/Game/Levels/AdvMultiplication/L08mul_eq_zero.lean
@@ -23,3 +23,12 @@ Statement mul_eq_zero (a b : ℕ) (h : a * b = 0) : a = 0 ∨ b = 0 := by
  Hint (hidden := true) "Now the goal can be deduced from `h2` by pure logic, so use the `tauto`
  tactic."
  tauto
+
+Conclusion "Here's the short proof:
+```
+have h2 := mul_ne_zero a b
+tauto
+```
+This works because, given `mul_ne_zero a b`,
+the argument is reduced to pure logic.
+"