diff --git a/Game/Levels/AdvMultiplication/L04one_le_of_ne_zero.lean b/Game/Levels/AdvMultiplication/L04one_le_of_ne_zero.lean
index 97de4141..a4c836d4 100644
--- a/Game/Levels/AdvMultiplication/L04one_le_of_ne_zero.lean
+++ b/Game/Levels/AdvMultiplication/L04one_le_of_ne_zero.lean
@@ -21,5 +21,5 @@ Statement one_le_of_ne_zero (a : ℕ) (ha : a ≠ 0) : 1 ≤ a := by
   Hint (hidden := true) "Now take apart the existence statement with `cases ha with n hn`."
   cases ha with n hn
   use n
-  rw [hn, succ_eq_add_one, add_comm]
-  rfl
+  rw [add_comm, <-succ_eq_add_one]
+  exact hn