[STATEMENT]
lemma s_gt_0: "s > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < s
[PROOF STEP]
using \<epsilon>_range
[PROOF STATE]
proof (prove)
using this:
\<epsilon> \<in> {0<..<1}

goal (1 subgoal):
 1. 0 < s
[PROOF STEP]
by (simp add:s_def)