diff --git a/src/lean4/human_eval/problem_2.lean b/src/lean4/human_eval/problem_2.lean
index cd021b0..3185ef3 100644
--- a/src/lean4/human_eval/problem_2.lean
+++ b/src/lean4/human_eval/problem_2.lean
@@ -23,14 +23,14 @@ def problem_spec
 (number: Rat) :=
 -- spec
 let spec (res) :=
+number > 0 →
 0 ≤ res ∧
 res < 1 ∧
 number.floor + res = number;
-number > 0 →
 -- program terminates
-(∃ result, impl number = result ∧
+∃ result, impl number = result ∧
 -- return value satisfies spec
-spec result)
+spec result
 -- end_def problem_spec
 
 -- start_def generated_spec