diff --git a/Game/Levels/L18Pset/L06.lean b/Game/Levels/L18Pset/L06.lean
index 5a470b3..94b8a37 100644
--- a/Game/Levels/L18Pset/L06.lean
+++ b/Game/Levels/L18Pset/L06.lean
@@ -15,7 +15,7 @@ DisabledTheorem MonotoneSeriesEven
 
 /-- Prove `MonotoneSeriesEven`
 -/
-Statement {a : ℕ → ℝ} (ha : Antitone a) (apos : ∀ n, 0 ≤ a n) :
+Statement {a : ℕ → ℝ} (ha : Antitone a) :
   Monotone (fun n ↦ ∑ k ∈ range (2 * n), (-1)^k * a k) := by
 apply Monotone_of_succ
 intro n
diff --git a/Game/Levels/L18Pset/L07.lean b/Game/Levels/L18Pset/L07.lean
index b92f4a0..80df2d6 100644
--- a/Game/Levels/L18Pset/L07.lean
+++ b/Game/Levels/L18Pset/L07.lean
@@ -17,7 +17,7 @@ DisabledTheorem AntitoneSeriesOdd
 
 /-- Prove `AntitoneSeriesOdd`
 -/
-Statement {a : ℕ → ℝ} (ha : Antitone a) (apos : ∀ n, 0 ≤ a n) : Antitone (fun n ↦ ∑ k ∈ range (2 * n + 1), (-1)^k * a k) := by
+Statement {a : ℕ → ℝ} (ha : Antitone a) : Antitone (fun n ↦ ∑ k ∈ range (2 * n + 1), (-1)^k * a k) := by
 apply Antitone_of_succ
 intro n
 induction' n with n hn