proposition: Lemma starting_segment_exists x (Cx: cond x): exists l, << SORTED: StronglySorted r l >> /\ << INIT: forall x', cond x' /\ r^* x' x <-> In x' l >>.
proof: Proof. destruct STO as [[IRR T] TOT]. assert (WF: well_founded (restr_rel cond r)). by eauto using wf_restr, fsupp_well_founded. apply fsupp_restr with (cond:=cond) in FSUPP. induction x using (well_founded_induction WF). destruct (classic (min_elt (restr_rel cond r) x)). * exists (x :: nil); repeat split; ins; desf; vauto. rewrite clos_refl_transE in H2; desf; eauto. apply clos_trans_of_transitiveD in H2; eauto; firstorder. * forward eapply fsupp_immediate_pred as [y [M N]]; eauto using fsupp_restr, irreflexive_restr, transitive_restr. specialize_full H; eauto; red in M; desf. exists (l ++ x :: nil); splits; ins. rewrite StronglySorted_app_iff, StronglySorted_cons_iff; splits; ins; desf; vauto. apply INIT in IN1; desf. apply ct_of_trans, ct_end; vauto. rewrite in_app_iff, <- INIT; ins. intuition; desf; eauto using clos_refl_trans. tertium_non_datur (y = x') as [|NEQ]; desf; eauto using clos_refl_trans. apply TOT in NEQ; desf; eauto using clos_refl_trans. apply rt_of_trans in H2; ins; red in H2; desf; eauto. destruct (N x'); vauto. Qed.
imports: HahnBase HahnSets HahnList HahnRelationsBasic HahnWf HahnMinElt HahnEquational HahnSorted