proposition: Lemma starting_segment_contains_endpoint x (Cx: cond x) : In x (starting_segment Cx).
proof: Proof. apply in_starting_segment_iff; vauto. Qed.
imports: HahnBase HahnSets HahnList HahnRelationsBasic HahnWf HahnMinElt HahnEquational HahnSorted