proposition: Lemma initial_prefix X Y (Xwo: well_ordered X) (sub: Y ≺ X): ∃ x, x ∈ X ∧ ¬x ∈ Y ∧ Y ≌ restrict x X.
proof: Proof. assert (Proper (equ ==> iff) (λ x, x ∈ X ∧ ¬x ∈ Y)) as diff_impl by solve_proper. set (exist _ _ diff_impl: set) as diff. destruct (wo_minima X Xwo diff) as [m [[inX notinY] lb]]. - firstorder. - destruct (classic (∃ x, x ∈ diff)) as [|none]; trivial. destruct sub as [sub [ ]]. split; [|firstorder]. intros x inx. destruct (classic (x ∈ Y)); trivial. contradict none; exists x; split; trivial. - exists m; do 2 (split; trivial). destruct sub as [[sub closed] neq]. apply subset_equ; intros y iny. + split; auto. destruct (wo_lt_ge X Xwo y m) as [|contra]; auto. now eapply cs_closed in contra; eauto. + destruct iny as [iny bound]. destruct (classic (y ∈ Y)) as [|contra]; auto. enough (y ≺ y) as [ ]%irreflexivity. eapply lt_le_trans; eauto. apply lb; split; trivial. Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)