diff --git a/Game/Levels/AdvMultiplication/L05le_mul_right.lean b/Game/Levels/AdvMultiplication/L05le_mul_right.lean index 8540e23..d22d88b 100644 --- a/Game/Levels/AdvMultiplication/L05le_mul_right.lean +++ b/Game/Levels/AdvMultiplication/L05le_mul_right.lean @@ -19,7 +19,7 @@ TheoremDoc MyNat.le_mul_right as "le_mul_right" in "≤" Introduction " In Prime Number World we will be proving that $2$ is prime. -To do this, we will have to rule out things like $2 ≠ 37 × 42.$ +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.