Library Zermelo1904
1904 Proof by Jonas Kaiser
We did some minimal re-arrangements, but all lemmas, proofs and comments were given by Jonas Kaiser.Lemma cp (A B : Prop) : A -> B <-> ~ B -> ~ A.
Proof. split; intros H.
+ intros nb a. auto.
+ intros a. apply NNPP. intros nb. now apply H.
Qed.
Lemma notex2all (X : Type) (P : X -> Prop) : (~ exists x, P x) ->
forall x, ~ P x.
Proof. intros C x px. apply C. now exists x. Qed.
Lemma notall2ex (X : Type) (P : X -> Prop) : (~ forall x, P x) ->
exists x, ~ P x.
Proof. intros C. apply NNPP. intros C'. apply C. intros x.
apply NNPP. intros npx. apply C'. now exists x.
Qed.
Variable X : Type.
Variable Eps : (X -> Prop) -> X.
Variable EpsR : forall P : X -> Prop, forall x : X, P x -> P (Eps P).
Variable EpsExt : forall P Q : X -> Prop, (forall x, P x <-> Q x) -> Eps P = Eps Q.
Definition X' : X -> Prop := fun _ => True.
Definition E : X -> Prop := fun _ => False.
Definition Sing (a : X) := fun x => a = x.
Definition SubP (A B : X -> Prop) := forall x, A x -> B x.
Infix "c=" := SubP (at level 70).
Lemma SubP_trans (A B C : X -> Prop) : A c= B -> B c= C -> A c= C.
Proof. intros H1 H2 x H. now apply H2, H1. Qed.
Variable P_ext : forall A B: X -> Prop, A c= B -> B c= A -> A = B.
Definition SatP (A: X -> Prop) := exists x, A x.
Lemma E_or_Sat (A: X -> Prop) : A = E \/ SatP A.
Proof. destruct (classic (SatP A)); auto. left. apply P_ext.
- intros a a_A. apply H. now exists a.
- intros e [].
Qed.
Definition BU (A B : X -> Prop) := fun x => A x \/ B x.
Definition DiffP (A B : X -> Prop) := fun x : X => A x /\ ~ B x.
Infix "--" := DiffP (at level 40).
Definition Rel := X -> X -> Prop.
Lemma DiffP_SubP_left A B : (A -- B) c= A.
Proof. now intros z [H _]. Qed.
Lemma DiffP_empty A : A -- E = A.
Proof. apply P_ext.
- intros x H; apply H.
- intros x H. split; auto.
Qed.
Lemma DiffP_full A : A -- A = E.
Proof. apply P_ext.
- intros x [H NH]. destruct (NH H).
- intros x [].
Qed.
Lemma DiffP_full_inv A B : A -- B = E -> A c= B.
Proof. intros H a a_A. destruct (classic (B a)); auto.
assert (C: E a) by ( rewrite <- H; unfold DiffP; auto).
destruct C.
Qed.
Lemma DiffP_not_in A B x : ~ (A -- B) x -> A x -> B x.
Proof. intros H J. apply NNPP. intros K. apply H; now split. Qed.
Lemma not_in_DiffP (A B: X -> Prop) x : B x -> ~ (A -- B) x.
Proof. intros H C. now apply C. Qed.
Lemma DiffP_SubP_mono A B C : A c= B -> A -- C c= B -- C.
Proof. intros H x x_D. split.
+ apply H, x_D.
+ apply x_D.
Qed.
Lemma DiffP_BU_restore A B : B c= A -> BU (A -- B) B = A.
Proof. intros H. apply P_ext; intros x K.
+ destruct K.
- apply H0.
- now apply H.
+ destruct (classic (B x)).
- now right.
- left. now split.
Qed.
Section RelProps.
Variable U : X -> Prop.
Variable R : Rel.
Definition trich := forall a b, U a -> U b ->
(R a b <-> ~ R b a /\ a <> b) /\ (a = b <-> ~ R a b /\ ~ R b a).
Definition trans := forall a b c, U a -> U b -> U c ->
R a b -> R b c -> R a c.
Definition lin := trich /\ trans.
Definition hasLeast := exists a, U a /\ forall b, U b -> ~ R b a.
End RelProps.
Definition wellOrdered (U : X -> Prop) (R : Rel) :=
lin U R /\ forall V, SatP V -> V c= U -> hasLeast V R.
Lemma wf_ind (U : X -> Prop) (R : Rel) : wellOrdered U R ->
forall P : X -> Prop,
(forall x, U x -> (forall y, U y -> R y x -> P y) -> P x) ->
forall x, U x -> P x.
Proof. intros [_ L] P H.
set (C := fun x => U x /\ ~ P x).
assert (K: C c= U) by (now intros c [J _]).
destruct (E_or_Sat C) as [Eq|J].
+ subst.
intros x x_U. apply NNPP. intros NPx.
assert (H': E x) by (rewrite <- Eq; auto). apply H'.
+
destruct (L C J K) as [t [[t_U NPt] tMin]]. exfalso.
apply NPt, H; auto. intros u u_U Rut.
apply NNPP. intros W. apply (tMin u); auto. unfold C; auto.
Qed.
Definition IS (U : X -> Prop) (a: X) (R : Rel) (x : X) :=
U x /\ R x a.
Definition GS (U : X -> Prop) (R: Rel) :=
wellOrdered U R /\ (forall a, U a -> a = Eps (X' -- IS U a R)).
Lemma union_split' (M R A B C : X -> Prop):
(forall x, M x -> R x -> A x \/ B x \/ C x) ->
(forall x, M x -> R x -> A x) \/
(exists x, M x /\ R x /\ B x) \/
(exists x, M x /\ R x /\ C x).
Proof. intros H.
destruct (classic (exists x, (M x /\ R x) /\ (B x \/ C x)))
as [[x [[m r] [b|c]]]|F].
+ right. left. exists x. tauto.
+ right. right. exists x. tauto.
+ left. intros x m r. destruct (H x m r) as [a|[b|c]].
- assumption.
- exfalso. apply F. exists x. tauto.
- exfalso. apply F. exists x. tauto.
Qed.
Lemma union_split (R A B C : X -> Prop):
(forall x, R x -> A x \/ B x \/ C x) ->
(forall x, R x -> A x) \/
(exists x, R x /\ B x) \/
(exists x, R x /\ C x).
Proof. intros H.
destruct (classic (exists x, R x /\ (B x \/ C x)))
as [[x [r [b|c]]]|F].
+ right. left. exists x. tauto.
+ right. right. exists x. tauto.
+ left. intros x r. destruct (H x r) as [a|[b|c]].
- assumption.
- exfalso. apply F. exists x. tauto.
- exfalso. apply F. exists x. tauto.
Qed.
Lemma IS_trans M R x y z : trans M R -> IS M y R z ->
M x -> M y -> R y x -> IS M x R z.
Proof. unfold IS. intros T [z_m zRy] x_m y_m yRz.
split; try assumption. now apply T with (b:=y).
Qed.
Lemma SubP_Eq_strict A B : A c= B -> A = B \/ SatP (B -- A).
Proof. intros C. destruct (classic (SatP (B -- A))); auto.
left. apply P_ext; auto. intros b b_B. apply NNPP.
intros nb_A. apply H. exists b. now split.
Qed.
Lemma trich_not M R a b : trich M R -> M a -> M b -> ~ R a b ->
R b a \/ a = b.
Proof. intros T a_m b_m H.
destruct (T _ _ a_m b_m) as [_ [_ F]].
destruct (classic (R b a)); auto.
Qed.
Lemma GS_IS M a R : GS M R -> M a -> GS (IS M a R) R.
Proof. intros [[[Tri Tra] L] G] a_M.
assert (K: IS M a R c= M) by now intros z [z_M _].
split; try split; try split.
+ intros x y x_I y_I. apply Tri; auto.
+ intros x y z x_I y_I z_I. apply Tra; auto.
+ intros V neV K'.
assert (K'': V c= M) by now apply SubP_trans with (B:=IS M a R).
now apply L.
+ intros x x_I. assert (x_M : M x) by apply x_I.
rewrite (G x x_M) at 1 .
apply EpsExt. intros z; split; intros [_ nz_I].
- split; try exact I. intros z_I'. apply nz_I.
split; apply z_I'.
- split; try exact I. intros z_I'. apply nz_I.
destruct z_I' as [z_M J].
repeat split; auto. apply Tra with (b:=x); auto. apply x_I.
Qed.
Definition iseg M' M R := exists a, M a /\ IS M a R = M'.
Lemma iseg_irefl M R : trich M R -> ~ iseg M M R.
Proof. intros T [a [a_M Eq]]. rewrite <- Eq in a_M.
destruct a_M as [a_M Raa]. now apply T in Raa.
Qed.
Lemma iseg_nocyc M1 M2 R1 R2 : trich M1 R1 ->
iseg M1 M2 R2 -> ~ iseg M2 M1 R1.
Proof. intros T [a [a_M1 Eq1]] [b [b_M2 Eq2]].
assert (C : M1 = M2) by (apply P_ext;
[rewrite <- Eq1|rewrite <- Eq2]; now intros z [z_Z]).
rewrite <- C in Eq2. apply (iseg_irefl T). exists b; auto.
Qed.
Lemma iseg_sub M' M R : iseg M' M R -> M' c= M.
Proof. intros [x [_ Eq]]. rewrite <- Eq; now intros z [z_Z _]. Qed.
Lemma IS_compare (M1 M2 : X -> Prop) (R1 R2: Rel) :
GS M1 R1 -> GS M2 R2 ->
(M1 = M2) \/ iseg M2 M1 R1 \/ iseg M1 M2 R2.
Proof. intros g1 g2.
assert (lemma : forall x, M1 x ->
(M2 x /\ IS M1 x R1 = IS M2 x R2) \/
(exists x1, (IS M1 x R1) x1 /\ IS M1 x1 R1 = M2) \/
(IS M1 x R1 = M2)).
+ destruct g1 as [W1 g1]. specialize (wf_ind W1). intros wf.
apply wf. intros x x_m1 IH. apply union_split' in IH.
destruct IH as [IH|[IH|IH]].
- assert (L1: IS M1 x R1 c= M2) by
(intros z [A B]; now destruct (IH z A B)).
destruct (SubP_Eq_strict L1) as [Eq|H].
* right. now right.
* destruct g2 as [[Li2 J] g2]. apply J in H. {
destruct H as [t [K K']].
pose proof (DiffP_SubP_left K) as t_M2.
assert (L2: IS M1 x R1 = IS M2 t R2).
+ apply P_ext.
- intros a a_S1. pose proof (L1 a a_S1) as a_M2.
split; auto. destruct (classic (R2 a t)); auto. exfalso.
destruct Li2 as [T _].
destruct (trich_not _ _ T a_M2 t_M2 H) as [H'|H'].
* assert (t_S2 : IS M2 a R2 t) by now split.
destruct a_S1. destruct (IH a H0 H1). apply K.
apply IS_trans with (y:=a); auto. apply W1.
now rewrite H3.
* apply K; congruence.
- intros b b_S2. destruct (classic (IS M1 x R1 b)); auto.
exfalso. assert (b_D : (M2 -- IS M1 x R1) b) by
(split; auto; apply b_S2).
apply K' in b_D. apply b_D, b_S2.
+ left. apply DiffP_SubP_left in K.
pose proof (g1 _ x_m1) as E. rewrite L2 in E.
rewrite <- (g2 t K) in E. split; congruence.
}
apply DiffP_SubP_left.
- destruct IH as [y [ym1 [y_r1_x [x1 [A B]]]]]. right. left.
exists x1. split; try assumption. apply IS_trans with (y:=y);
try assumption. now destruct W1 as [[_ T] _].
- destruct IH as [y [y_m1 [y_R1_x H]]]. right. left. exists y.
split; try assumption. now split.
+ apply union_split in lemma. destruct lemma as [L|[L|L]].
- set (S := fun y : X => exists z, M1 z /\ IS M1 z R1 y).
set (T1 := M1 -- S). set (T2 := M2 -- S).
assert (H1 : S c= M1) by (intros y [z [_ y_S1z]]; apply y_S1z).
assert (H2 : T1 c= M1) by (intros z H; apply H).
assert (H3 : T2 c= M2) by (intros z H; apply H).
assert (H4 : M1 c= M2) by (intros z H; now apply L).
pose proof (SubP_trans H1 H4) as H5.
destruct (E_or_Sat T1) as [H6|H6].
* pose proof (DiffP_full_inv H6) as H7.
pose proof (P_ext H1 H7) as H8.
destruct (E_or_Sat T2) as [H9|H9].
{ pose proof (DiffP_full_inv H9) as H10.
pose proof (P_ext H5 H10) as H.
left; congruence. }
{ remember H9 as H9'; clear HeqH9'. apply g2 in H9'; auto.
destruct H9' as [t [t_T2 t_min]]. right. right.
exists t; split; auto. rewrite <- H8.
apply P_ext; intros a a_H.
+ assert (H10: ~ T2 a) by
(intros J; apply (t_min a J), a_H).
apply DiffP_not_in with (A:=M2); auto. apply a_H.
+ assert (H10: ~ T2 a) by (now apply not_in_DiffP).
split; auto. destruct (classic (R2 a t)); auto. exfalso.
apply trich_not with (M:= M2) in H; auto; try apply g2.
destruct H.
- apply t_T2. exists a; split; auto.
destruct (L a) as [_ Eq]; auto. rewrite Eq.
split; auto.
- congruence. }
* remember H6 as H6'; clear HeqH6'. destruct H6' as [t H6'].
assert (H7: T1 = Sing t).
{ apply P_ext; intros t' H.
+ destruct (classic (R1 t t')) as [R1tt'|nR1tt'].
- exfalso. apply (@not_in_DiffP M1 S t); auto.
exists t'; split; auto; split; auto.
- apply trich_not with (M:= M1) in nR1tt'; auto.
* destruct nR1tt'; auto. exfalso.
apply (@not_in_DiffP M1 S t'); auto. exists t; split;
auto; split; auto.
* apply g1.
+ congruence. }
{ assert (H8 : T1 c= T2) by (now apply DiffP_SubP_mono).
assert (H9 : T2 t) by (now apply H8).
destruct (classic (SatP (T2 -- Sing t))).
+ assert (H10: T2 -- Sing t c= M2) by
(apply SubP_trans with (B:=T2); auto;
apply DiffP_SubP_left).
apply g2 in H; auto. destruct H as [t' [t'_D t'_min]].
destruct (classic (R2 t t')).
- assert (t_min : forall b : X, T2 b -> ~ R2 b t).
* intros u u_D uR2t.
destruct g2 as [[[tri tra] _] _ ]. unfold trich in tri.
assert (J1: M2 u) by auto. assert (J2: M2 t) by auto.
destruct (tri u t J1 J2) as [F _]. apply F in uR2t.
destruct uR2t. apply (t'_min u). split; auto.
destruct (classic (u = t')); try congruence.
exfalso. apply (t'_min u). split; auto.
unfold trans in tra. apply (tra u t t'); auto.
apply F; split; auto.
* assert (H11: IS M2 t R2 = S).
{ apply P_ext; intros a a_H.
+ assert (H12: ~ T2 a) by
(intros J; apply (t_min a J), a_H).
apply DiffP_not_in with (A:=M2); auto. apply a_H.
+ assert (H12: ~ T2 a) by (now apply not_in_DiffP).
split; auto. destruct (classic (R2 a t)); auto.
exfalso. apply trich_not with (M:= M2) in H0;
auto; try apply g2. destruct H0.
- apply H9. exists a; split; auto.
destruct (L a) as [_ Eq]; auto. rewrite Eq.
split; auto.
- congruence. }
{ assert (H12 : BU (Sing t) (IS M2 t R2) = M1).
+ rewrite <- H7, H11. now apply DiffP_BU_restore.
+ right. right. exists t'. split; auto. symmetry.
apply P_ext; intros x K.
- rewrite <- H12 in K. destruct K.
* rewrite <- H0. split; auto.
* destruct H0. split; auto.
destruct g2 as [[[_ tra] _] _ ].
apply tra with (b:=t); auto.
- destruct K. destruct (classic (x = t)).
* rewrite H14; auto.
* destruct (classic (R2 x t)).
{ rewrite <- H12. right. split; auto. }
{ destruct g2 as [[[tri tra] _] _ ].
assert (H16: R2 t x) by (apply tri; auto).
exfalso. apply (t'_min x); auto.
split; auto. split; auto.
rewrite <- H11. intros [_ C].
now apply H15. } }
- apply trich_not with (M:=M2) in H; auto; try apply g2.
exfalso. destruct H.
* destruct (L t) as [_ Eq]; auto.
assert (H11 : IS M1 t R1 t') by
(rewrite Eq; split; auto).
apply DiffP_SubP_left in t'_D. apply t'_D.
exists t; split; auto.
* apply t'_D. congruence.
+ assert (H10: T2 = Sing t).
- apply P_ext; intros t'' J.
* destruct (classic (t = t'')); auto. exfalso.
apply H. exists t''. split; auto.
* congruence.
- left. rewrite <- (DiffP_BU_restore H1). fold T1.
rewrite <- (DiffP_BU_restore H5). fold T2.
congruence. }
- destruct L as [x [x_M1 [x1 [S L]]]]. right. left. exists x1.
split; auto. apply S.
- destruct L as [x [x_M1 L]]. right. left. exists x; auto.
Qed.
Corollary IS_compare' M1 M2 R1 R2 : GS M1 R1 -> GS M2 R2 ->
~ iseg M2 M1 R1 -> M1 = M2 \/ iseg M1 M2 R2.
Proof. intros g1 g2 H.
destruct (IS_compare g1 g2) as [K|[K|K]]; auto.
congruence.
Qed.
Corollary IS_share (M1 M2 : X -> Prop) (R1 R2: Rel) :
GS M1 R1 -> GS M2 R2 -> forall a : X, M1 a /\ M2 a ->
(IS M1 a R1 = IS M2 a R2).
Proof. intros g1 g2 a [a_M1 a_M2].
pose proof (GS_IS a g1 a_M1) as g1'.
pose proof (GS_IS a g2 a_M2) as g2'.
destruct (IS_compare g1' g2')
as [Eq|[[z [z_I Eq]]|[z [z_I Eq]]]].
+ assumption.
+ assert (C: z = a).
- destruct g2 as [_ G2]. destruct g1' as [_ G1'].
now rewrite (G2 a a_M2), (G1' z z_I), Eq.
- destruct z_I as [z_M1 Rza]. destruct g1 as [[[T1 _] _] _].
apply T1 in Rza; auto. destruct Rza.
+ assert (C: z = a).
- destruct g1 as [_ G1]. destruct g2' as [_ G2'].
now rewrite (G1 a a_M1), (G2' z z_I), Eq.
- destruct z_I as [z_M2 Rza]. destruct g2 as [[[T2 _] _] _].
apply T2 in Rza; auto. destruct Rza.
Qed.
Definition W : Rel := fun a b => exists Ma Ra, GS Ma Ra /\ Ma a /\
forall Mb Rb, GS Mb Rb -> Mb b -> iseg Ma Mb Rb.
Definition L (x : X) := exists M, M x /\ GS M W.
Lemma tautW1' P Q R : ~ (P /\ Q /\ R) -> P -> Q -> ~ R.
Proof. auto. Qed.
Lemma tautW1 a b Ma Ra : ~ W a b -> GS Ma Ra -> Ma a ->
exists Mb Rb, GS Mb Rb /\ Mb b /\ ~ iseg Ma Mb Rb.
Proof. intros nWab gma a_Ma. unfold W in nWab.
specialize (notex2all _ nWab Ma). intros H.
specialize (notex2all _ H Ra). intros H'.
specialize (tautW1' H' gma a_Ma). intros H''.
apply notall2ex in H''. destruct H'' as [Mb H''].
apply notall2ex in H''. destruct H'' as [Rb H''].
exists Mb, Rb. tauto.
Qed.
Lemma trich1W a b : W a b -> ~ W b a /\ a <> b.
Proof. intros [Ma [Ra [gma [a_Ma H]]]]. split; intros K.
+ destruct K as [Mb [Rb [gmb [b_Mb H']]]].
specialize (H Mb Rb gmb b_Mb). specialize (H' Ma Ra gma a_Ma).
refine (iseg_nocyc _ H H'). apply gma.
+ assert (b_Ma : Ma b) by congruence.
specialize (H Ma Ra gma b_Ma).
assert (trich Ma Ra) by apply gma.
now apply iseg_irefl in H.
Qed.
Lemma L_trich' a b : L a -> L b -> (W a b <-> ~ W b a /\ a <> b).
Proof. intros a_L b_L. split.
+ apply trich1W.
+ intros [nWba nEqab].
destruct a_L as [Ma [a_Ma gma]].
destruct b_L as [Mb [b_Mb gmb]].
assert (TriB : trich Mb W) by apply gmb.
destruct (tautW1 nWba gmb b_Mb)
as [La [Ra [gla [a_La S]]]].
assert (C: La c= Mb).
- destruct (IS_compare' gla gmb S).
* subst; now intros z z_Z.
* now apply iseg_sub in H.
- assert (a_Mb : Mb a) by auto.
apply TriB; auto.
Qed.
Lemma L_trich : trich L W.
Proof. intros a b a_L b_L. split.
+ now apply L_trich'.
+ assert (L' : ~ W a b <-> W b a \/ a = b) by
(destruct (L_trich' a_L b_L) as [F G]; tauto).
split.
- intros Eab. split.
* apply L'; auto.
* intros Wba. destruct (L_trich' b_L a_L) as [F _].
destruct (F Wba). congruence.
- intros [nWab nWba]. apply L' in nWab.
destruct nWab; congruence.
Qed.
Lemma transW M : trans M W.
Proof. intros a b c a_M b_M c_M Wab Wbc.
destruct Wab as [Ma [Ra [gma [a_Ma H]]]].
destruct Wbc as [Mb [Rb [gmb [b_Mb H']]]].
destruct (H Mb Rb gmb b_Mb) as [b' [b'_Mb Eq]].
exists Ma, Ra. split; auto. split; auto.
intros Mc Rc gmc c_Mc.
destruct (H' Mc Rc gmc c_Mc) as [c' [c'_Mc Eq']].
assert (C : Mb c= Mc) by (rewrite <- Eq'; now intros z [K _]).
exists b'. split; auto. rewrite <- Eq. apply IS_share; auto.
Qed.
Corollary L_trans : trans L W.
Proof. apply (transW L). Qed.
Lemma L_lin : lin L W.
Proof. split.
+ apply L_trich.
+ apply L_trans.
Qed.
Lemma L_least L' : SatP L' -> L' c= L -> hasLeast L' W.
Proof. intros [a a_L'] C.
set (L'' := fun x => IS L' a W x \/ x = a).
assert (C' : L'' c= L') by
(intros z [z_I|Eq]; try congruence; apply z_I).
assert (H : L a) by now apply C.
destruct H as [M' [a_M' gm']].
assert (C'': L'' c= M').
+ intros x [x_I|Eq]; try congruence.
assert (Wxa : W x a) by apply x_I.
destruct Wxa as [Mx [Rx [gmx [x_Mx H]]]].
specialize (H M' W gm' a_M'). apply iseg_sub in H; auto.
+ assert (minL'' : hasLeast L'' W)
by (apply gm'; auto; exists a; now right).
destruct minL'' as [t [t_L'' mt]].
exists t. split; auto. intros b b_L' Wbt.
apply (mt b); auto.
destruct (classic (L'' b)) as [H|H]; auto. exfalso.
apply not_or_and in H. destruct H as [H1 H2].
apply not_and_or in H1. destruct H1; auto.
assert (H' : W a b) by (apply L_trich; auto).
assert (H'' : W a t) by (apply L_trans with (b:=b); auto).
destruct t_L'' as [[H0 H1]|Eq]; try congruence.
destruct (@L_trich a t) as [F _]; auto. now apply F in H''.
Qed.
Lemma L_wo : wellOrdered L W.
Proof. split.
+ apply L_lin.
+ apply L_least.
Qed.
Lemma L_gamma : GS L W.
Proof. split.
+ apply L_wo.
+ intros a [Ma [a_Ma gma]].
assert (Eq : IS L a W = IS Ma a W).
- apply P_ext; intros x [x_Z Wxa].
* split; auto. destruct Wxa as [Mx [Rx [gmx [x_Mx H]]]].
specialize (H Ma W gma a_Ma). now apply (iseg_sub H).
* split; auto. exists Ma; auto.
- rewrite Eq. now apply gma.
Qed.
Lemma L_super : X' c= L.
Proof. intros x _. destruct (classic (L x)) as [x_L|nx_L]; auto.
exfalso.
assert (x_C : (X' -- L) x) by (unfold X'; split; auto).
set (m := Eps (X' -- L)).
assert (m_C : (X' -- L) m) by (apply (EpsR _ x x_C)).
set (L' := fun x => L x \/ x = m).
assert (m_L' : L' m) by (now right).
assert (nEqm : forall x, L' x -> x <> m -> L x) by
(intros y y_L' nEqym; destruct y_L' as [y_L|Eqym]; congruence).
assert (nm_L : ~ L m) by apply m_C.
assert (H : forall a, L' a -> a <> m -> W a m).
+ intros a a_L' nEqam.
destruct (nEqm a a_L' nEqam) as [Ma [a_Ma gma]].
exists Ma, W. split; auto; split; auto.
intros Mm Rm gmm m_Mm.
destruct (classic (iseg Ma Mm Rm)) as [K|K]; auto. exfalso.
assert (J : Mm c= Ma).
- destruct (IS_compare' gmm gma K) as [Eq'|J'].
* subst. now intros b bM.
* now apply iseg_sub in J'.
- assert (m_Ma : Ma m) by auto.
assert (m_L : L m) by (exists Ma; auto).
now apply nm_L.
+ assert (tra : trans L' W) by apply (transW L').
assert (tri1 : forall a b, L' a -> L' b -> W a b ->
~ W b a /\ a <> b) by (intros a b a_L' b_L' Wab;
apply (trich1W Wab)).
assert (tri2 : forall a b, L' a -> L' b -> ~ W b a /\ a <> b ->
W a b).
- intros a b a_L' b_L' [nWba nEqab].
destruct (classic (a = m)) as [Eqam | nEqam];
destruct (classic (b = m)) as [Eqbm | nEqbm].
* congruence.
* rewrite Eqam in nWba. apply H in nEqbm; congruence.
* rewrite Eqbm. now apply H.
* apply nEqm in nEqam; auto. apply nEqm in nEqbm; auto.
apply L_trich'; auto.
- assert (tri : trich L' W).
* intros a b a_L' b_L'.
pose proof (tri1 a b a_L' b_L') as F.
pose proof (tri2 a b a_L' b_L') as G.
assert (J : ~ W a b <-> W b a \/ a = b) by tauto.
split; split; auto.
{ intros Eqab. split.
+ apply J; auto.
+ intros Wba. apply (tri1 b a b_L' a_L') in Wba.
destruct Wba; congruence. }
{ intros [nWab nWba]. tauto. }
* assert (least : forall V, SatP V -> V c= L' -> hasLeast V W).
{ intros V [v v_V] C.
destruct (classic (V m)) as [m_V|nm_V].
+ set (S := IS V m W). destruct (E_or_Sat S) as [EqS|neS].
- exists m. split; auto. intros b b_V Wbm.
assert (C': E b)
by (rewrite <- EqS; unfold S; split; auto).
destruct C'.
- assert (J : S c= IS L' m W)
by (intros s [s_V Wsm]; split; auto).
assert (J' : IS L' m W c= L) by (intros s [s_L' Wsm];
destruct (tri1 s m s_L' (C m m_V) Wsm) as [_ K];
now apply nEqm).
assert (J'' : S c= L)
by (intros s s_S; apply J', J, s_S).
destruct (L_least neS J'') as [ms [ms_S mP]].
assert (ms_V : V ms) by now destruct ms_S.
assert (mP' : forall b, V b -> ~ W b ms).
* intros b b_V Wbms.
assert (Wmsm : W ms m) by apply ms_S.
assert (Wbm : W b m)
by (apply tra with (b:=ms); auto).
assert (b_S : S b) by (split; auto).
assert (nWbms : ~ W b ms) by now apply mP.
contradiction.
* exists ms; split; auto.
+ assert (C' : V c= L).
- intros y y_V. assert (nEqym : y <> m) by congruence.
apply (nEqm y (C y y_V) nEqym).
- apply L_least; auto. now exists v. }
{ assert (wo : wellOrdered L' W)
by (split; try split; auto).
assert (gamma : forall a : X, L' a ->
a = Eps (X' -- IS L' a W)).
+ intros a a_L'.
destruct (classic (a = m)) as [Eqam|nEqam].
- assert (J : IS L' a W c= L) by (intros y [y_L' Wya];
destruct (tri1 y a y_L' a_L' Wya) as [_ K];
apply nEqm; congruence).
assert (J' : L c= IS L' a W).
* intros y y_L. assert (y_L' : L' y) by now left.
split; auto. rewrite Eqam. apply (H y); auto.
congruence.
* assert (EqLIS : L = IS L' a W) by now apply P_ext.
now rewrite <- EqLIS, Eqam.
- assert (J : IS L' a W c= L).
* intros y [y_L' Wya]. specialize (H a a_L' nEqam).
assert (Wym : W y m) by now apply tra with (b:=a).
destruct (tri1 y m y_L' m_L' Wym) as [_ K].
now apply nEqm.
* assert (EqII : IS L' a W = IS L a W).
{ apply P_ext; intros z z_I.
+ assert (Wza : W z a) by apply z_I.
split; auto.
+ destruct z_I as [z_L Waz]. split; auto.
now left. }
{ rewrite EqII. now apply L_gamma, nEqm. }
+ assert (gl' : GS L' W). split; auto.
assert (m_L : L m) by (exists L'; now split).
contradiction. }
Qed.
Theorem X_wo : wellOrdered X' W.
Proof. assert (Eq : X' = L).
+ apply P_ext.
- apply L_super.
- intros x _; unfold X'; auto.
+ rewrite Eq. apply L_wo.
Qed.