From 88021db205c4ab236da6d6f20db116efba5e3653 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sat, 15 Feb 2025 16:48:31 +0000 Subject: [PATCH] docs: more hints in advanced multiplication L5 --- Game/Levels/AdvMultiplication/L05le_mul_right.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Game/Levels/AdvMultiplication/L05le_mul_right.lean b/Game/Levels/AdvMultiplication/L05le_mul_right.lean index 0b77212..334cc67 100644 --- a/Game/Levels/AdvMultiplication/L05le_mul_right.lean +++ b/Game/Levels/AdvMultiplication/L05le_mul_right.lean @@ -23,7 +23,8 @@ of proving that $2$ is prime. To do this, we will have to rule out things like $2 = 37 × 42.$ We will do this by proving that any factor of $2$ is at most $2$, which we will do using this lemma. The proof I have in mind manipulates the hypothesis -until it becomes the goal, using pretty much everything which we've proved in this world so far. +until it becomes the goal, using `mul_left_ne_zero`, `one_le_of_ne_zero` and +`mul_le_mul_right`. " Statement le_mul_right (a b : ℕ) (h : a * b ≠ 0) : a ≤ a * b := by