proposition: Lemma segment_property x (Cx: cond x) y (Cy: cond y): ⟪SORTED: StronglySorted r (segment Cx Cy)⟫ /\ ⟪SEGMENT: forall z, cond z /\ r x z /\ r＊ z y <-> In z (segment Cx Cy)⟫.
proof: Proof. ins; splits. by apply StronglySorted_filterP, starting_segment_property. split; ins; desf. * apply in_filterP_iff; split. by apply starting_segment_property. intro N; apply starting_segment_property in N; desf. destruct STO as [[IRR T] TOT]. apply clos_refl_transE in N0; desf; eauto. apply clos_trans_of_transitiveD in N0; eauto. * unfold segment in H; apply in_filterP_iff in H; desf. apply starting_segment_property in H; desf; splits; try done. eby eapply not_in_starting_segment. Qed.
imports: HahnBase HahnSets HahnList HahnRelationsBasic HahnWf HahnMinElt HahnEquational HahnSorted