proposition: Lemma in_segment_iff x (Cx: cond x) y (Cy: cond y) z : In z (segment Cx Cy) <-> cond z /\ r x z /\ r^* z y.
proof: Proof. symmetry; apply segment_property. Qed.
imports: HahnBase HahnSets HahnList HahnRelationsBasic HahnWf HahnMinElt HahnEquational HahnSorted