docs: more hints in advanced multiplication L5

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