proposition: Lemma not_in_starting_segment x (Cx: cond x) y (Cy: cond y): ~ In y (starting_segment Cx) -> r x y.
proof: Proof. ins; apply NNPP; intro. destruct H; apply starting_segment_property. split; ins. destruct STO as [[IRR T] TOT]. specialize (TOT _ Cx _ Cy). apply imply_to_or in TOT; desf; clarify_not; vauto. Qed.
imports: HahnBase HahnSets HahnList HahnRelationsBasic HahnWf HahnMinElt HahnEquational HahnSorted