proposition: Lemma in_starting_segment_iff x (Cx: cond x) z : In z (starting_segment Cx) <-> cond z /\ r＊ z x.
proof: Proof. symmetry; apply starting_segment_property. Qed.
imports: HahnBase HahnSets HahnList HahnRelationsBasic HahnWf HahnMinElt HahnEquational HahnSorted