[STATEMENT]
lemma nonempty_fine_imp_less: "\<lbrakk>fine \<delta> (a, b) D; D \<noteq> []\<rbrakk> \<Longrightarrow> a < b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fine \<delta> (a, b) D; D \<noteq> []\<rbrakk> \<Longrightarrow> a < b
[PROOF STEP]
apply (induct set: fine, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b c D a x. \<lbrakk>fine \<delta> (b, c) D; D \<noteq> [] \<Longrightarrow> b < c; a < b; a \<le> x; x \<le> b; b - a < \<delta> x; (a, x, b) # D \<noteq> []\<rbrakk> \<Longrightarrow> a < c
[PROOF STEP]
apply (drule fine_imp_le, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done