From 2d18d49436c72707ef6af0564a578fb59c25ab70 Mon Sep 17 00:00:00 2001
From: David Renshaw <dwrenshaw@gmail.com>
Date: Mon, 20 Nov 2023 09:20:06 -0500
Subject: [PATCH] [Imo1968P5] the constant of periodicity must be positive

---
 Compfiles/Imo1968P5.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/Compfiles/Imo1968P5.lean b/Compfiles/Imo1968P5.lean
index bb16d7c4..61e0070b 100644
--- a/Compfiles/Imo1968P5.lean
+++ b/Compfiles/Imo1968P5.lean
@@ -28,11 +28,12 @@ holds for all x.
 namespace Imo1968P5
 
 abbrev P (a : ℝ) (f : ℝ → ℝ) : Prop :=
-  ∀ x, f (x + a) = 1/2 + Real.sqrt (f x - (f x)^2)
+  0 < a ∧ ∀ x, f (x + a) = 1/2 + Real.sqrt (f x - (f x)^2)
 
 determine solution_func : ℝ → ℝ := sorry
 
-problem imo1968_p5a (f : ℝ → ℝ) (a : ℝ) (hf : P a f) : ∃ b, f.Periodic b := by
+problem imo1968_p5a (f : ℝ → ℝ) (a : ℝ) (hf : P a f) :
+    ∃ b, 0 < b ∧ f.Periodic b := by
   sorry
 
 problem imo1968_p5b :