[STATEMENT]
lemma simplex_segment:
   "\<exists>n. n simplex closed_segment a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. n simplex closed_segment a b
[PROOF STEP]
using simplex_segment_cases
[PROOF STATE]
proof (prove)
using this:
(if ?a = ?b then 0 else 1) simplex closed_segment ?a ?b

goal (1 subgoal):
 1. \<exists>n. n simplex closed_segment a b
[PROOF STEP]
by metis