(*** file order.v, version of november 10th, 2003---Carlos Simpson ***)


Require Export Arith.
Require Export groundwork7. 
Require Export notation9. 

Set Implicit Arguments. 


Module Order.
Export Umorphism.
Export Notation.Order_notation.





Definition property := [a:E; l:E -> E -> Prop]
(A (x:E)(inc x a) -> (l x x)
(A (x,y:E)(inc x a) -> (inc y a) -> (l x y) -> (l y x) -> x == y
   (x,y,z:E)(inc x a) -> (inc y a) -> (inc z a) -> (l x y) -> (l y z) -> (l x z)
)).

Definition axioms := [a:E]
(A (x:E)(inc x (U a)) -> (leq a x x)
(A (x,y:E)(leq a x y) -> (inc x (U a)) 
(A (x,y:E)(leq a x y) -> (inc y (U a))
(A (x,y:E)(leq a x y) -> (leq a y x) -> x == y
   (x,y,z:E)(leq a x y) -> (leq a y z) -> (leq a x z)
)))).

Lemma create_axioms : (a:E; l: E-> E->Prop)(property a l) -> (axioms (create a l)).
ir. uf axioms. dj. cluc. ap leq_create_if; Try am. ufi property H.
ee. ap H; am. ufi leq H1. xe. ufi leq H2; xe. Assert (inc x a).
LApply(H1 x y). ir. cluc. am. am. Assert (inc y a).
LApply(H2 x y). ir; cluc; am. am. ufi property H; ee.
ap H7. am. am. rwi leq_create_all H3; xe. rwi leq_create_all H4; xe.
Assert (inc x a). LApply(H1 x y); ir. cluc; am. am.
Assert (inc y a). LApply(H2 x y). ir. cluc; am. am.
Assert (inc z a). LApply(H2 y z); ir. cluc; am. am.
ufi property H; ee. ap leq_create_if. am. am. Apply H10 with y.
am. am. am. rwi leq_create_all H4; xe. rwi leq_create_all H5; xe.
Save. 





Lemma lt_leq_trans : (a,x,y,z:E)(axioms a) -> 
(lt a x y) -> (leq a y z) ->  (lt a x z).
ir. uf lt; ufi lt H0; ee. ufi axioms H; ee.
Apply H6 with y; au. uf not; ir. rwi H3 H0.
ufi axioms H; ee. ap H2. rw H3. ap H6; au.
Save.

Lemma leq_lt_trans : (a,x,y,z:E)(axioms a) -> 
(leq a x y) -> (lt a y z) -> (lt a x z).
ir. uf lt; ufi lt H1; ee. ufi axioms H; ee.
Apply H6 with y; au. uf not; ir. ap H2. wr H3.
wri H3 H1. ufi axioms H; ee. ap H6. Exact H1. Exact H0.
Save.




Lemma leq_refl : (a,x:E)(axioms a) -> (inc x (U a)) -> (leq a x x).
ir. ufi axioms H; xe. ap H; am.
Save.

Lemma leq_trans : (a,x,y,z:E)(axioms a) -> (leq a x y) -> (leq a y z) -> (leq a x z).
ir. ufi axioms H; ee. Apply H5 with y. Exact H0. Exact H1.
Save. 

Lemma leq_leq_eq : (a,x,y:E)(axioms a) -> (leq a x y) -> (leq a y x) -> x == y.
Intros.
Unfold axioms in H; xe. ap H4; am.
Save.



Lemma no_lt_leq : (a,x,y:E)(axioms a) -> (lt a x y) -> (leq a y x) -> False.
ir. ufi axioms  H; ufi lt H0; xe. ap H2; ap H5; am.
Save. 

Lemma leq_eq_or_lt : (a,x,y:E)(axioms a) -> (leq a x y) -> (x==y) \/ (lt a x y).
ir. Apply by_cases with x==y. ir. ap or_introl; am.
ir. ap or_intror. uf lt; xe.
Save. 

Module SetOfOrders.

Section orders_on_section. 
Variable x: E. 

Definition is_order_on := [a:E]
(A (axioms a)
(A (U a) == x
   (like a)
)). 

Definition little_leq := [lq:x->x->Prop; u,v:E]
(A (inc u x)
(A (inc v x)
   (hu : (inc u x); hv :(inc v x))(lq (B hu) (B hv))
)).

Definition lit_lq := [a:E; m,n:x](leq a (R m) (R n)).

Lemma create_little_leq : (a:E)(is_order_on a) ->
a == (create x (little_leq (lit_lq a))).
ir. 
Assert (leq a) == (little_leq (lit_lq a)).
ap arrow_extensionality; Intro u. 
ap arrow_extensionality; Intro v. 
ap iff_eq; ir. ufk leq H0; ee. 
ufk is_order_on H; ee. 
uhg; ee. wr H3; am. wr H3; am. 
ir. uhg. rw B_eq. rw B_eq. am. 
ufi little_leq H0; ee. 
Remind '(H2 H0 H1).  ufi lit_lq H3. 
rwi B_eq H3. rwi B_eq H3. am. 

wr H0. uh H. ee. wr H1. 
Exact H2. 
Save. 


Lemma is_order_bounded: (Bounded.axioms (is_order_on)). 
ir. 
Apply Bounded.little_criterion with x->x->Prop
[lq : x -> x-> Prop](create x (little_leq lq)). 
ir. sh '(lit_lq y).
sy; ap create_little_leq. am. 
Save. 

Definition orders_on := (Bounded.create is_order_on). 
 


Lemma inc_orders_on : (a:E)(inc a orders_on) ==
(is_order_on a). 
ir. 
uf orders_on. 
ap Bounded.inc_create. 
ap is_order_bounded. 
Save.

End orders_on_section.


End SetOfOrders. Export SetOfOrders. 


Module Morphisms.

Definition mor_axioms := [u:E]
(A (axioms (source u))
(A (axioms (target u))
(A (Umorphism.strong_axioms u)
   (x,y:E)(leq (source u) x y) -> (leq (target u) (ev u x) (ev u y))
))).

Lemma mor_Umor : (u:E)(mor_axioms u) -> (Umorphism.strong_axioms u).
Intros. Unfold mor_axioms in H; ee. Exact H1. 
Save. 
Coercion mor_Umor_C := mor_Umor.

Lemma identity_axioms : (a:E)(axioms a) -> (mor_axioms (Umorphism.identity a)).
ir. cx. uf mor_axioms; ee; clst. am. am.
ap identity_strong_axioms. ir. rw ev_identity. rw ev_identity.
am. Apply H2 with x. am. Apply H1 with y; am.
Save. 


Definition composable := [u,v:E]
(A (mor_axioms u)
(A (mor_axioms v)
   (source u) == (target v)
)).

Lemma compose_axioms : (u,v:E)(composable u v) -> (mor_axioms (Umorphism.compose u v)).
Intros.
Unfold composable in H; ee.
Unfold mor_axioms in H; ee.
Unfold mor_axioms in H0; ee.
Unfold mor_axioms; ee.
Rewrite -> source_compose; au.

Rewrite -> target_compose; au.

Apply Umorphism.compose_strong_axioms.
Unfold Umorphism.composable; ee.
Apply Umorphism.axioms_from_strong; am.
Apply Umorphism.axioms_from_strong; am.

am.

Intros.
Rewrite -> target_compose.
Rewrite -> ev_compose.
Rewrite -> ev_compose.
Rewrite -> source_compose in H8.
Apply H4.
Rewrite -> H1.
Apply H7.
am.

Unfold axioms in H0; ee.
Rewrite -> source_compose in H8.
Apply H10 with x; au.

Rewrite -> source_compose in H8.
Unfold axioms in H0; ee.
Apply H9 with y; au.
Save.

End Morphisms. Export Morphisms. 

Module Suborders. 

Definition suborder := [b,a:E](create b (leq a)).

Lemma suborder_axioms : (a,b:E)(axioms a) -> (sub b (U a)) -> (axioms (suborder b a)).
Intros.
Unfold suborder.
Apply create_axioms.
Unfold property.
Unfold axioms in H.
ee. ir; au.
ir. ap H3. Exact H7. Exact H8.
Intros.
Apply H4 with y; au.
Save.

Lemma underlying_suborder : (a,b:E)(U (suborder b a)) == b.
Intros.
Unfold suborder; Rewrite -> underlying_create; tv.
Save. 

Lemma leq_suborder_if : (a,b,x,y:E)(inc x b) -> (inc y b) -> (sub b (U a)) -> 
(leq a x y) -> (leq (suborder b a) x y).
Intros.
Unfold suborder.
Apply leq_create_if; au.
Save.

Lemma leq_suborder_then : (a,b,x,y:E)(axioms a) -> (sub b (U a)) ->
(leq (suborder b a) x y) ->
(A (inc x b)
(A (inc y b)
   (leq a x y)
)).
Intros.
ee.
Unfold suborder in H1.
Pose (leq_create_then H1).
ee; am.

Unfold suborder in H1.
Pose (leq_create_then H1); ee; am.

Unfold suborder in H1.
Pose (leq_create_then H1); ee; am.
Save.



Lemma leq_suborder_all : (a,b,x,y:E)(axioms a) -> (sub b (U a)) ->
(leq (suborder b a) x y) ==
(A (inc x b)
(A (inc y b)
   (leq a x y)
)).
Intros.
Apply iff_eq; Intros.
Pose _:=(leq_suborder_then H H0 H1).
ee; am.

Apply leq_suborder_if; ee; am.
Save.


Definition suborder_inclusion := [b,a:E](Umorphism.inclusion (suborder b a) a).

Lemma suborder_inclusion_mor_axioms : (a,b:E)(axioms a) -> (sub b (U a)) ->
(mor_axioms (suborder_inclusion b a)).
Intros.
Unfold suborder_inclusion.
Unfold mor_axioms; ee.
Unfold inclusion; Rewrite -> source_create.
Apply suborder_axioms; au.

Unfold inclusion; Rewrite -> target_create.
am.

Unfold inclusion.
Apply Umorphism.create_strong_axioms.
Unfold Umorphism.property.
Unfold Transformation.axioms.
Intros.
Rewrite -> underlying_suborder in H1.
Apply H0; au.

Intros.
Unfold inclusion.
Rewrite -> target_create.
Repeat Rewrite -> ev_create.
Unfold inclusion in H1; Rewrite -> source_create in H1.
Rewrite -> leq_suborder_all in H1.
ee.

am.

am. am.

Unfold inclusion in H1; Rewrite -> source_create in H1.
Rewrite -> leq_suborder_all in H1; au.
ee.
Rewrite -> underlying_suborder; am.

Unfold inclusion in H1; Rewrite -> source_create in H1.
Rewrite -> leq_suborder_all in H1; au.
ee.
Rewrite -> underlying_suborder; au.
Save.


Definition is_suborder := [a,b:E]
(A (axioms a)
(A (axioms b)
(A (sub (U a) (U b))
   (mor_axioms (Umorphism.inclusion a b))
))).

Lemma is_suborder_leq : (a,b,x,y:E)(is_suborder a b) -> 
(leq a x y) -> (leq b x y).
ir.
ufi is_suborder H.
ee.
ufi mor_axioms H3; ee.
Assert b==(target (inclusion a b)).
uf inclusion; rw target_create.
tv.

rw H7.
Assert x==(mapping (inclusion a b) x).
uf inclusion; rw ev_create; tv.
ufi leq H0.
ee.
am.

Assert y==(mapping (inclusion a b) y).
uf inclusion; rw ev_create; tv.
ufi leq H0; xe.

rw H8; rw H9.
ap H6.
uf inclusion; rw source_create; am.
Save. 

Lemma show_is_suborder : (a,b:E)(axioms a) -> (axioms b) -> 
((x,y:E)(leq a x y) -> (leq b x y)) -> (is_suborder a b).
ir. uf is_suborder; ee. am. am. uf sub; ir. Assert (leq b x x).
ap H1. ap leq_refl; am. ufi leq H3; xe. uf inclusion. uf mor_axioms. rw source_create.
rw target_create. ee. am. am. ap Umorphism.create_strong_axioms.
uf Umorphism.property. uf Transformation.axioms. ir. Assert (leq b x x).
ap H1. ap leq_refl; am. ufi leq H3; xe. ir. rw ev_create.
rw ev_create. ap H1; am. ufi leq H2; xe. ufi leq H2; xe.
Save. 

(*** note that this doesn't imply that the order on (U a) is the same as that induced by the
order on (U b) ****)

Lemma suborder_is_suborder : (a,b:E)(axioms a) -> (sub b (U a)) ->
(is_suborder (suborder b a) a).
ir. uf is_suborder. ee. ap suborder_axioms; am. uf suborder. am. uf suborder.
rw underlying_create. am.
Change (mor_axioms (suborder_inclusion b a)). ap suborder_inclusion_mor_axioms; am.
Save.

Lemma is_suborder_refl : (a:E)(axioms a) -> (is_suborder a a).
ir. uf is_suborder; dj. am. am. uf sub; ir; am. uf mor_axioms; dj.
uf inclusion; rw source_create. am. uf inclusion; rw target_create; am.
uf inclusion; ap create_strong_axioms. uf Umorphism.property. uf Transformation.axioms; ir; am.
uf inclusion; rw ev_create. rw ev_create. rw target_create. ufi inclusion H6. rwi source_create H6. am.
ufi inclusion H6; rwi source_create H6. ufi leq H6; ee. am. ufi inclusion H6; rwi source_create H6.
ufi leq H6; ee; am.
Save.

Lemma is_suborder_trans : (a,b,c:E)(is_suborder a b) -> (is_suborder b c) ->
(is_suborder a c).
ir. ap show_is_suborder. ufi is_suborder H; xe. ufi is_suborder H0; xe.
ir. Apply is_suborder_leq with b. am. Apply is_suborder_leq with a.
Exact H. Exact H1.
Save. 

Definition same_order := [a,b:E](A (is_suborder a b) (is_suborder b a)).

Lemma same_order_refl : (a:E)(axioms a) -> (same_order a a).
ir. uf same_order; ee. ap is_suborder_refl. am. ap is_suborder_refl; am.
Save.

Lemma same_order_symm : (a,b:E)(same_order a b) -> (same_order b a).
ir. ufi same_order H. uf same_order. ee. am. Exact H.
Save.

Lemma same_order_trans : (a,b,c:E)(same_order a b) -> (same_order b c) -> (same_order a c).
ir. ufi same_order H. ufi same_order H0. uf same_order. ee. Apply is_suborder_trans with b.
Exact H. Exact H0. Apply is_suborder_trans with b. Exact H1. Exact H2.
Save.


Lemma same_underlying : (a,b:E)(same_order a b) -> (U a) == (U b).
ir.
ufi same_order H; ee.
ufi is_suborder H.
ufi is_suborder H0.
ee.
ap extensionality.
am.

am.
Save. 

Lemma same_leq_eq : (a,b,x,y:E)(same_order a b) ->(leq a x y) == (leq b x y).
ir.
ap iff_eq; ir.
ufi same_order H.
ee.
Apply is_suborder_leq with a; am.

ufi same_order H; ee.
Apply is_suborder_leq with b; am.
Save.  

Lemma same_order_extens : (a,b:E)(same_order a b) -> (like a) 
-> (like b) -> a==b. 
ir. Assert (U a) == (U b). ap same_underlying; am. 
Assert (leq a) == (leq b). ap arrow_extensionality. 
ir. ap arrow_extensionality. ir. 
ap same_leq_eq. am. uh H0. rw H0. rw H2. 
rw H3. sy. Exact H1. 
Save. 

Lemma same_as_suborder_is_suborder : (a,b,x:E)(sub x (U b))-> (axioms b) -> 
(same_order a (suborder x b)) -> (is_suborder a b).
ir. Apply is_suborder_trans with (suborder x b). ufi same_order H1; ee.
Exact H1. ap suborder_is_suborder. Exact H0. am.
Save. 


Lemma suborder_trans : (a,b,c:E)(axioms c) -> (sub a b) -> (sub b (U c)) ->
(same_order (suborder a (suborder b c)) (suborder a c)).
ir. uf same_order; ee; ap show_is_suborder. ap suborder_axioms. ap suborder_axioms.
am. am. uf suborder; rw underlying_create. am. ap suborder_axioms. am. uf sub; ir; au.
ir. ap leq_suborder_if. rwi leq_suborder_all H2. ee; am. ap suborder_axioms; am.
uf suborder; rw underlying_create. am. rwi leq_suborder_all H2; ee. am.
ap suborder_axioms; am. uf suborder; rw underlying_create. am. uf sub; ir; au.
rwi leq_suborder_all H2; ee. rwi leq_suborder_all H4; ee. am. am. am. ap suborder_axioms; am.
uf suborder; rw underlying_create; uf sub; ir; au. ap suborder_axioms. am.
uf sub; ir; au. ap suborder_axioms. ap suborder_axioms; am. uf suborder; rw underlying_create.
am. ir. rwi leq_suborder_all H2; ee. ap leq_suborder_if; au. uf suborder; rw underlying_create; am.
ap leq_suborder_if. au. au. am. am. am. uf sub; ir; au.
Save.



End Suborders. Export Suborders. 


Module Linear.


Definition is_linear := [a:E]
(A (axioms a)
   (x,y:E)(inc x (U a)) -> (inc y (U a)) -> ((leq a x y) \/ (leq a y x))
).

Lemma linear_axioms : (a:E)(is_linear a) -> (axioms a).
Intros. Unfold is_linear in H; ee; am. Save.
Coercion linear_axioms_C := linear_axioms.

Lemma linear_not_lt_leq :(a,x,y:E)(is_linear a) -> (inc x (U a)) -> (inc y (U a)) -> 
((lt a x y) -> False) -> (leq a y x).
Intros.
Unfold is_linear in H; ee.
Pose (H3 ? ? H0 H1).
NewInduction o.
Pose (leq_eq_or_lt H H4).
NewInduction o.
Rewrite -> H5.
Unfold axioms in H; ee. ap H; am.

Elim (H2 H5).

am.
Save.

Lemma injective_lt_lt : (u,x,y:E)(mor_axioms u) -> (Umorphism.injective u) ->
(lt (source u) x y) -> (lt (target u) (ev u x) (ev u y)).
ir.
ufi lt H1. uf lt; ee. ufi mor_axioms H; xe.
ap H5. am. uf not; Intros. ufi injective H0; ee.
ufi Transformation.injective H4. ee. ufi Transformation.injects H5.
ap H2. ap H5. ufi mor_axioms H; ee. ufi axioms H; ee.
Apply H9 with y. am. ufi mor_axioms H; ee.
ufi axioms H; ee. Apply H10 with x; au. am.
Save. 

Lemma linear_injective_leq_back : (u,x,y:E)(mor_axioms u) -> (Umorphism.injective u) ->
(is_linear (source u)) -> (inc x (U (source u))) -> (inc y (U (source u))) ->
(leq (target u) (ev u x) (ev u y)) -> (leq (source u) x y).
Intros.
Apply linear_not_lt_leq; au.
Intros.
Pose (injective_lt_lt H H0 H5).
Apply no_lt_leq with (target u) (ev u y) (ev u x).
Assert (mor_axioms u).
am.

Unfold mor_axioms in H6; ee.

am.

am.

am.
Save. 

Lemma linear_injective_lt_back : (u,x,y:E)(mor_axioms u) -> (Umorphism.injective u) ->
(is_linear (source u)) -> (inc x (U (source u))) -> (inc y (U (source u))) ->
(lt (target u) (ev u x) (ev u y)) -> (lt (source u) x y).
Intros.
Unfold lt in H4.
Unfold lt; ee.
Apply linear_injective_leq_back; au.

Unfold not; Intros.
Apply H5.
Rewrite -> H6; tv.
Save. 


Definition is_linear_subset := [a,b:E]
(A (axioms a)
(A (sub b (U a))
   (is_linear (suborder b a))
)).

Lemma linear_sub: (a,b,c:E)(is_linear_subset a b) -> (sub c b) ->
(is_linear_subset a c).
ir.
ufi is_linear_subset H; uf is_linear_subset; dj; ee.
am.

uf sub; ir; au.

ufi is_linear H4; uf is_linear; dj; ee.
ap suborder_axioms; am.

Assert (inc x (U (suborder b a))).
rw underlying_suborder.
ap H0.
rwi underlying_suborder H6.
am.

Assert (inc y (U (suborder b a))).
rw underlying_suborder.
ap H0.
rwi underlying_suborder H7; am.

Remind '(H8 x y H9 H10).
nin H11.
ap or_introl.
rwi underlying_suborder H6.
rwi underlying_suborder H7.
ap leq_suborder_if; Try am.
rwi leq_suborder_all H11; ee.
am.

am.

am.

ap or_intror.
rwi underlying_suborder H6.
rwi underlying_suborder H7.
rw leq_suborder_all.
rwi leq_suborder_all H11.
xd.

am.

am.

am.

am.
Save. 

End Linear. Export Linear. 

Module Bounds. 


Definition is_minimal := [a,b,x:E]
(A (axioms a)
(A (sub b (U a))
(A (inc x b)
   (y:E)(inc y b) -> (leq a y x) -> y == x
))).

Lemma minimal_axioms : (a,b,x:E)(is_minimal a b x) -> (axioms a).
Intros. Unfold is_minimal in H; ee; am. Save.
Coercion minimal_axioms_C := minimal_axioms.


Definition is_maximal := [a,b,x:E]
(A (axioms a)
(A (sub b (U a))
(A (inc x b)
   (y:E)(inc y b) -> (leq a x y) -> x == y
))).

Lemma maximal_axioms : (a,b,x:E)(is_maximal a b x) -> (axioms a).
Intros. Unfold is_maximal in H; ee; am. Save.
Coercion maximal_axioms_C := maximal_axioms.



Definition is_upper_bound := [a,b,x:E]
(A (axioms a)
(A (sub b (U a))
(A (inc x (U a))
   (y:E)(inc y b) -> (leq a y x)
))).

Lemma upper_bound_axioms : (a,b,x:E)(is_upper_bound a b x) -> (axioms a).
Intros. Unfold is_upper_bound in H; ee; am. Save.
Coercion upper_bound_axiomsC := upper_bound_axioms.

Definition is_lower_bound := [a,b,x:E]
(A (axioms a)
(A (sub b (U a))
(A (inc x (U a))
   (y:E)(inc y b) -> (leq a x y)
))).

Lemma lower_bound_axioms : (a,b,x:E)(is_lower_bound a b x) -> (axioms a).
Intros. Unfold is_lower_bound in H; ee; am. Save.
Coercion lower_bound_axiomsC := lower_bound_axioms.



Definition is_bottom_element := [a,b,x:E]
(A (is_lower_bound a b x)
   (inc x b)
). 

Lemma bottom_element_lower_bound : (a,b,x:E)(is_bottom_element a b x) -> (is_lower_bound a b x).
Intros. Unfold is_bottom_element in H; ee; am. Save.
Coercion bottom_element_lower_boundC := bottom_element_lower_bound.

Definition is_top_element := [a,b,x:E]
(A (is_upper_bound a b x)
   (inc x b)
).

Lemma top_element_upper_bound : (a,b,x:E)(is_top_element a b x) -> (is_upper_bound a b x).
Intros. Unfold is_top_element in H; ee; am. Save.
Coercion top_element_upper_boundC := top_element_upper_bound.



Lemma top_element_maximal : (a,b,x:E)(is_top_element a b x) -> (is_maximal a b x).
Intros. Unfold is_top_element in H. Unfold is_upper_bound in H. Unfold is_maximal.
ee. Intros. am. am. am. ir. ufi axioms H; ee. ap H8. am. ap H3; am.
Save. 

Coercion top_element_maximalC := top_element_maximal. 

Lemma bottom_element_minimal : (a,b,x:E)(is_bottom_element a b x) -> (is_minimal a b x).
Intros. Unfold is_bottom_element in H. Unfold is_lower_bound in H. Unfold is_minimal.
xe. Intros. Unfold axioms in H; xe. ap H8. am. ap H3. am. 
Save. 

Coercion bottom_element_minimalC := bottom_element_minimal.

Lemma top_element_unique : (a,b,x,y:E)(is_top_element a b x) -> (is_top_element a b y) -> x == y.
Intros. Unfold is_top_element in H H0; xe. Unfold is_upper_bound in 
H H0; xe. Unfold axioms in H; xe. ap H11.
ap H6; am.

ap H8; am.
Save. 

Lemma bottom_element_unique : (a,b,x,y:E)(is_bottom_element a b x) -> (is_bottom_element a b y) -> x == y.
Intros. Unfold is_bottom_element in H H0; xe. Unfold is_lower_bound in 
H H0; xe. Unfold axioms in H; xe. ap H11.
ap H8; am.

ap H6; am.
Save. 

Lemma linear_maximal_top_element : (a,b,x:E)(is_linear a) -> (is_maximal a b x) -> (is_top_element a b x).
Intros. Unfold is_linear in H. Unfold is_maximal in H0. 
Unfold is_top_element. Unfold is_upper_bound. xd. Intros. 
Assert (inc x (U a)). Apply H1; au. Assert (inc y (U a)). Apply H1; au. 
Pose (H2 ? ? H6 H7). NewInduction o. uh H. ee. 
 Assert x == y. 
Apply H4; au. Rewrite H13. ap H; am.  am. 
Save.

Lemma linear_minimal_bottom_element : (a,b,x:E)(is_linear a) -> (is_minimal a b x) -> (is_bottom_element a b x).
Intros. Unfold is_linear in H. Unfold is_minimal in H0. 
Unfold is_bottom_element. Unfold is_lower_bound. xd. Intros. 
Assert (inc x (U a)). Apply H1; au. Assert (inc y (U a)). Apply H1; au. 
Pose (H2 ? ? H6 H7). NewInduction o. Unfold axioms in H; xe. Assert y == x. 
Apply H4; au. Rewrite H9.  Unfold axioms in H; ee.  ap H. am. 
Save.


Definition downward_subset := [a,x:E]
(Z (U a) [y:E](leq a y x)).

Definition punctured_downward_subset := [a,x:E]
(Z (U a) [y:E](lt a y x)).

Definition downward_suborder := [a,x:E](suborder (downward_subset a x) a).

Definition punctured_downward_suborder := [a,x:E](suborder (punctured_downward_subset a x) a).




End Bounds. Export Bounds. 

Module WellOrdered. 


Definition is_well_ordered := [a:E]
(A (is_linear a)
   (b:E)(sub b (U a)) -> (nonempty b) -> (exists [x:E](is_bottom_element a b x))
).

Lemma wo_linear : (a:E)(is_well_ordered a) -> (is_linear a).
Intros. Unfold is_well_ordered in H; xe. Save.
Coercion wo_linear_C := wo_linear.







Lemma bottom_element_no_lt : (a,b,x,y:E)(is_bottom_element a b x) -> 
(lt a y x) -> (inc y b) -> False.
Intros.
Unfold is_bottom_element in H; ee.
Unfold is_lower_bound in H; ee.
Assert (leq a x y).
Apply H5; am.
Apply no_lt_leq with a y x; au.
Save.




Definition choose_bottom_element := [a,b:E](choose [x:E](is_bottom_element a b x)).

Lemma wo_choose_bottom : (a,b:E)(is_well_ordered a) -> (sub b (U a)) -> (nonempty b) ->
(is_bottom_element a b (choose_bottom_element a b)).
Intros.
Unfold is_well_ordered in H; ee.
Pose (H2 b H0 H1).
Pose (choose_pr e).
am.
Save.

Lemma wo_induction : (a:E; H:(is_well_ordered a); p:E-> Prop)
((x:E)(inc x (U a)) -> ((y:E)(inc y (U a)) -> (lt a y x) -> (p y)) -> (p x)) ->
((x:E)(inc x (U a)) -> (p x)).
ir.
Pose b:=(Z (U a) [z:E]~(p z)). ap excluded_middle; uf not; ir.
Assert (nonempty b). Apply nonempty_intro with x. uf b.
Ztac. Pose z:=(choose_bottom_element a b).
Assert (is_bottom_element a b z). uf z; ap wo_choose_bottom.
am. uf b; ap Z_sub. am. Assert (sub b (U a)). uf b; ap Z_sub.
Assert (inc z b). ufi is_bottom_element H4; ee.
Assert (inc z (U a)). ap H5; am. am. Assert (not (p z)).
ufi b H6. Ztac. ap H7. ap H0; ir. au. ap excluded_middle; 
uf not; ir. Assert (inc y b). uf b; Ztac.
Apply bottom_element_no_lt with a b z y; au.
Save.



Definition is_wo_subset := [a,b:E]
(A (is_linear_subset a b)
   (is_well_ordered (suborder b a))
).





Lemma wo_same_order : (a,b:E)(same_order a b) -> (is_well_ordered a) -> (is_well_ordered b).
ir. uhg; dj. uhg; dj. 
ufi same_order H; ee. 
ufi is_suborder H; ee. 
am. Assert (leq b x y)==(leq a x y).
sy; ap same_leq_eq. am. Assert (leq b y x)==(leq a y x). sy; ap same_leq_eq; am.
rw H4. rw H5. uh H0. ee. uh H0; ee. ap H7. Assert (U a)==(U b). ap same_underlying.
am. rw H8; am. Assert (U a)==(U b). ap same_underlying; am. rw H8; am.
Assert (U a)==(U b). ap same_underlying; am. Assert (sub b0 (U a)). rw H4; am.
uh H0; ee. Remind '(H6 ? H5 H3). nin H7. sh x. uhg; ee. uhg; ee. uh H; ee. ufi is_suborder H; ee.
am. am. uh H7; ee. ap H2; am. ir. Assert (leq b x y)==(leq a x y). sy. ap same_leq_eq.
am. rw H9. uh H7. ee. uh H7. ee. ap H13. am. uh H7. ee. am.
Save. 





(*** a scale is a morphism between well ordered subsets that starts at the bottom and is injective with no gaps ***)

Definition is_scale := [u:E]
(A (mor_axioms u)
(A (Umorphism.injective u)
(A (is_well_ordered (source u))
(A (is_well_ordered (target u))
   (x,y:E)(inc x (U (source u))) -> (leq (target u) y (ev u x)) -> (exists [z:E](A (inc z (U (source u))) (ev u z) == y))
)))).

Lemma scale_mor_axioms : (u:E)(is_scale u) -> (mor_axioms u).
Intros. Unfold is_scale in H; ee; am. Save.
Coercion scale_mor_axiomsC := scale_mor_axioms.

Lemma scale_injective : (u:E)(is_scale u) -> (Umorphism.injective u).
Intros. Unfold is_scale in H; ee; am. Save.
Coercion scale_injectiveC := scale_injective.



Lemma scale_leq_back : (u,x,y:E)(is_scale u) -> (inc x (U (source u))) -> (inc y (U (source u))) ->
(leq (target u) (ev u x) (ev u y)) -> (leq (source u) x y).
Intros.
Unfold is_scale in H; ee.
Unfold is_well_ordered in H4; ee.
Apply linear_injective_leq_back; au.
Save.


Lemma scale_lt_back : (u,x,y:E)(is_scale u) -> (inc x (U (source u))) -> (inc y (U (source u))) ->
(lt (target u) (ev u x) (ev u y)) -> (lt (source u) x y).
Intros.
Unfold is_scale in H; ee.
Unfold is_well_ordered in H4; ee.
Apply linear_injective_lt_back; au.
Save.



Lemma scale_leq_ev : (u,v,x:E)(is_scale u) -> (is_scale v) -> (source u) == (source v) -> (target u) == (target v)
-> (inc x (U (source u))) -> (leq (target v) (ev u x) (ev v x)).
Intros.
Unfold is_scale in H H0; ee.
Apply (!wo_induction ? H9 [w:E](leq (target v) (ev u w) (ev v w))).
Intros.
Unfold is_well_ordered in H10; ee.
Unfold is_linear in H10; ee.
Apply linear_not_lt_leq.
Unfold is_well_ordered in H7; xe.

Unfold mor_axioms in H0; ee.
Unfold Umorphism.strong_axioms in H17; ee;
 Unfold Umorphism.axioms in H17.
Apply H17.
Rewrite <- H1; am.

Rewrite <- H2.
Unfold mor_axioms in H; ee.
Unfold Umorphism.strong_axioms in H17; ee.
ap H17; Exact H12.

Intros.
Unfold lt in H16; ee.
Rewrite <- H2 in H16.
Pose (H11 ? ? H12 H16).
NewInduction e.
ee.
Assert (lt (source u) x1 x0).
Apply scale_lt_back.
Unfold is_scale; ee.
am. Exact H5. Exact H9. 
Rewrite -> H2; am.

am.

am.
am. 
Rewrite -> H19.
Unfold lt; xe.

Assert (lt (target v) (ev v x1) (ev v x0)).
Apply injective_lt_lt.
am.

am.

Rewrite <- H1; am.

Assert (leq (target v) (ev u x1) (ev v x1)).
Apply H13.
am.

am.

Unfold lt in H21; ee.
Apply H23.
Apply leq_leq_eq with (target v).
wr H2.
am.

Exact H21.

wr H19.
Exact H22.

Exact H3.
Save.



Lemma scale_same_ev : (u,v,x:E)(is_scale u) -> (is_scale v) -> (source u) == (source v) -> (target u) == (target v)
-> (inc x (U (source u))) -> (ev u x)== (ev v x).
Intros.
Apply leq_leq_eq with (target u).
Unfold is_scale in H; ee.
Unfold mor_axioms in H; xe.

Rewrite -> H2.
Apply scale_leq_ev; au.

Apply scale_leq_ev; au.
Rewrite <- H1; am.
Save.

Lemma scale_unique : (u,v:E)(is_scale u) -> (is_scale v) -> (source u) == (source v) -> (target u) == (target v)
-> u == v.
Intros.
Apply Umorphism.extens.
Unfold is_scale in H; ee.
Unfold mor_axioms in H; xe.

Unfold is_scale in H0; ee.
Unfold mor_axioms in H0; xe.

am.

am.

Intros.
Apply scale_same_ev; au.
Save. 

Definition scale_subset := [a,b:E]
(A (is_well_ordered b)
(A (sub a (U b))
   (x,y:E)(inc y a) -> (leq b x y) -> (inc x a)
)).





Lemma source_suborder_inclusion : (a,b:E)(source (suborder_inclusion a b)) == (suborder a b).
ir.
uf suborder_inclusion.
uf inclusion; rw source_create.
tv.
Save.

Lemma target_suborder_inclusion : (a,b:E)(target (suborder_inclusion a b)) == b.
ir.
uf suborder_inclusion.
uf inclusion; rw target_create.
tv.
Save.

Lemma mapping_suborder_inclusion : (a,b,x:E)(inc x a) ->(mapping (suborder_inclusion a b) x) == x.
ir.
uf suborder_inclusion.
uf inclusion; rw ev_create.
tv.
rw underlying_suborder; am.
Save. 

Lemma suborder_well_ordered : (a,b:E)(sub a (U b)) -> (is_well_ordered b) -> (is_well_ordered (suborder a b)).
ir.
ufk is_well_ordered H0; ee.
ufk is_linear H0; ee.
uf is_well_ordered; dj.
uf is_linear; dj.
ap suborder_axioms; am.

rw leq_suborder_all.
rw leq_suborder_all.
Remind '(H2 x y).
LApply H6.
ir.
LApply H7; ir.
nin H8.
ap or_introl.
ee.
rwi underlying_suborder H4.
Exact H4.

rwi underlying_suborder H5; ap H5.

am.

ap or_intror.
ee.
rwi underlying_suborder H5; ap H5.

rwi underlying_suborder H4; ap H4.

am.

ap H.
rwi underlying_suborder H5; ap H5.

ap H.
rwi underlying_suborder H4; ap H4.

am.

am.

am.

am.

Assert (sub b0 (U b)).
uf sub; ir; ap H.
rwi underlying_suborder H4; ap H4.
am.

Remind '(H1 b0 H6 H5).
nin H7.
sh x.
uf is_bottom_element; dj.
uf is_lower_bound; dj.
ap suborder_axioms.
am.

am.

am.

ap H9.
ufi is_bottom_element H7; ee.
am.

rw leq_suborder_all; dj.
rwi underlying_suborder H9.
ap H9.
ufi is_bottom_element H7; ee.
am.

rwi underlying_suborder H9; ap H9; am.

ufi is_bottom_element H7; ee.
ufi is_lower_bound H7; ee.
ap H17.
am.

am.

am.

ufi is_bottom_element H7; ee; am.
Save. 


Lemma wo_sub: (a,b,c:E)(is_wo_subset a b) -> (sub c b) ->
(is_wo_subset a c).
ir. uh H. ee. uhg. dj. Apply linear_sub with b. am. am.
Apply wo_same_order with (suborder c (suborder b a)). ap suborder_trans.
uh H. ee. am. am. uh H. ee. am. ap suborder_well_ordered. rw underlying_suborder.
am. am.
Save. 

Lemma wo_sub_bottom : (a,b:E)(is_wo_subset a b) -> (nonempty b) ->
(is_bottom_element a b (choose_bottom_element a b)).
ir. Assert (exists [x:E](is_bottom_element a b x)). uh H; ee.
Pose y:=(choose_bottom_element (suborder b a) b). Assert (is_bottom_element (suborder b a) b y).
uf y. ap wo_choose_bottom. am. rw underlying_suborder. uf sub; ir; am. am. sh y.
uh H2. ee. uh H2; ee. uhg. ee. uhg; ee. uh H; ee. am. uh H; ee. am. uh H; ee.
ap H7; am. ir. Remind '(H6 ? H7). rwi leq_suborder_all H8; ee. am. uh H; ee; am.
uh H; ee; am. am. Remind '(choose_pr H1). Exact H2.
Save. 

Lemma scale_suborder_inclusion : (a,b:E)(scale_subset a b) -> 
(is_scale (suborder_inclusion a b)).
ir.
ufi scale_subset H; ee.
ufk is_well_ordered H.
ee.
ufk is_linear H; ee.
ufk axioms H; ee.
uf is_scale; dj.
ap suborder_inclusion_mor_axioms.
am.

am.

uf injective.
dj.
ufi mor_axioms H8; ee.
ufi strong_axioms H10; ee.
Exact H10.

uf Transformation.injective.
rw source_suborder_inclusion.
rw target_suborder_inclusion.
rw underlying_suborder.
dj.
uf Transformation.axioms.
ir.
rw mapping_suborder_inclusion.
ap H0; am.

am.

uf Transformation.injects.
ir.
rwi mapping_suborder_inclusion H13; Try am.
rw H13.
rw mapping_suborder_inclusion.
tv.

am.

rw source_suborder_inclusion.
ap suborder_well_ordered.
am.

am.

rw target_suborder_inclusion.
am.

sh y.
dj.
rw source_suborder_inclusion.
rw underlying_suborder.
Apply H1 with x.
rwi source_suborder_inclusion H12.
rwi underlying_suborder H12.
Exact H12.

rwi target_suborder_inclusion H13.
rwi mapping_suborder_inclusion H13.
Exact H13.

rwi source_suborder_inclusion H12.
rwi underlying_suborder H12.
Exact H12.

rw mapping_suborder_inclusion.
tv.

rwi source_suborder_inclusion H14.
rwi underlying_suborder H14.
Exact H14.
Save.


(*
Lemma empty_scale_subset : (a:E)(is_well_ordered a) -> (scale_subset emptyset a).

Save.

Lemma scale_subset_intersection2 : (a,u,v:E)(scale_subset u a) -> (scale_subset v a) ->
(scale_subset (intersection2 u v) a).

Save.

Definition is_scale_between := [a,b,f:E]
(A (is_well_ordered a)
(A (is_well_ordered b)
(A (is_scale f)
(A (source f) == a
   (target f) == b
)).

Lemma scale_between_compose : (a,b,c,f,g:E)(is_scale_between a b f) -> (is_scale_between b c g) ->
(is_scale_between a c (Umorphism.compose g f)).

Save.

Lemma scale_between_identity : (a,f:E)(is_scale_between a a f) -> f == (Umorphism.identity a).

Save.

Lemma scale_between_inverse : (a,b,f,g:E)(is_scale_between a b f) -> (is_scale_between b a g) ->
(Umorphism.are_inverse f g).

Save. 

Lemma scale_between_surjective_inverse : (a,b,f:E)(is_scale_between a b f) ->
(Umorphism.surjective f) -> (is_scale_between b a (Umorphism.inverse f)).

Save. 

Definition ordinal_leq := [a,b:E]
(exists [f:E](is_scale_between a b f)).


Lemma ordinal_leq_refl : (a:E)(is_well_ordered a) -> (ordinal_leq a a).

Save.

Lemma ordinal_leq_trans : (a,b,c:E)(ordinal_leq a b) -> (ordinal_leq b c) -> (ordinal_leq a c).

Save. 

Definition same_ordinal := [a,b:E]
(A (ordinal_leq a b) (ordinal_leq b a)).

Lemma same_ordinal_refl : (a:E)(is_well_ordered a) -> (same_ordinal a a).

Save.

Lemma same_ordinal_symm : (a,b:E)(same_ordinal a b) -> (same_ordinal b a).

Save.

Lemma same_ordinal_trans : (a,b,c:E)(same_ordinal a b) -> (same_ordinal b c) -> (same_ordinal a c).

Save. 

Definition correspond := [a,b,x,y:E]
(A (is_well_ordered a)
(A (is_well_ordered b)
(A (inc x (U a))
(A (inc y (U b))
   (same_ordinal (downward_suborder a x) (downward_suborder b y))
)))).

Definition corresponding := [a,b,x:E](choose [y:E](correspond a b x y)).

Definition has_correspondant := [a,b,x:E](exists [y:E](correspond a b x y)).

Lemma correspond_symm : (a,b,x,y:E)(correspond a b x y) -> (correspond b a y x).

Save.

Lemma correspond_refl : (a,x:E)(is_well_ordered a) -> (inc x (U a)) -> (correspond a a x x).

Save.

Lemma correspond_trans : (a,b,c,x,y,z:E)(correspond a b x y) -> (correspond b c y z) ->
(correspond a c x z).

Save. 

Lemma corresponding_unique : (a,b,x,y:E)(correspond a b x y) -> (corresponding a b x) == y.

Save. 


Lemma scale_correspond : (a,b,f,x:E)(is_scale_between a b f) -> (inc x (U a)) ->
(correspond a b x (ev f x)).

Save.

Lemma has_correspondant_leq : (a,b,x,u:E)(has_correspondant a b x) -> (leq a u x) ->
(has_correspondant a b u).

Save. 

Lemma has_correspondant_scale_subset : (a,b:E)(is_well_ordered a) -> (is_well_ordered b) ->
(scale_subset (Z (U a) [x:E](has_correspondant a b x)) a).

Save. 


Lemma have_correspondants_disj : (a,b:E)(is_well_ordered a) -> (is_well_ordered b) -> 
((x:E)(inc x (U a)) -> (has_correspondant a b x)) \/
((y:E)(inc y (U b)) -> (has_correspondant b a y)).

Save.

Lemma ordinal_leq_disj : (a,b:E)(is_well_ordered a) -> (is_well_ordered b) ->
(ordinal_leq a b) \/ (ordinal_leq b a).

Save.


*)


End WellOrdered. Export WellOrdered. 

Module Zorn.
 



Definition is_ultra_bound := [a,b,x:E]
(A (is_upper_bound a b x) ~(inc x b)).  

Definition ultra_bound := [a,b:E](choose [x:E](is_ultra_bound a b x)).
(*** here a is the order and b is the subset ***)

Definition eq_ultra_bound := [a,b,x:E](A (is_ultra_bound a b x) (ultra_bound a b) == x).

Definition is_ultra_zorn := [a:E]
(A (axioms a)
   (b:E)(is_linear_subset a b) -> (is_ultra_bound a b (ultra_bound a b))
).

Definition is_ultra_linear_subset := [a,b:E]
(A (is_wo_subset a b)
   (x:E)(inc x b) -> (eq_ultra_bound a (intersection2 b (punctured_downward_subset a x)) x)
).


Definition coincide_at := [a,b,c,x:E]
(A (inc x b)
(A (inc x c)
(A (y:E)(inc y b) -> (leq a y x) -> (inc y c)
   (y:E)(inc y c) -> (leq a y x) -> (inc y b)
))).

Definition coinciders := [a,b,c:E](Z b [x:E](coincide_at a b c x)).


Lemma coinciders_symm : (a,b,c:E)(coinciders a b c) == (coinciders a c b).
Assert (a,b,c,x:E)(coincide_at a b c x)->(coincide_at a c b x).
ir. uh H; uhg; xd.
Assert (a,b,c:E)(sub (coinciders a b c) (coinciders a c b)).
ir. uf sub; ir. uf coinciders. ufi coinciders H0. Ztac. ap Z_inc. uh H2; xd.
ap H. am. ir. ap extensionality. ap H0. ap H0.
Save.
 


Definition downward_saturated := [a,b,c:E]
(A (axioms a)
(A (sub b (U a))
(A (sub c b)
   (x,y:E)(inc x c) -> (inc y b) -> (leq a y x) -> (inc y c)
))).

Lemma coinciders_saturated : (a,b,c:E)(is_ultra_linear_subset a b) -> (is_ultra_linear_subset a c)->
(downward_saturated a b (coinciders a b c)).
ir.
uhg.
dj.
uh H; ee.
uh H; ee.
uh H; ee.
am.

uh H; ee.
uh H; ee.
uh H; ee.
am.

uhg; ir.
ufi coinciders H3; Ztac.

uf coinciders; ap Z_inc.
am.

uhg; ee.
am.

ufi coinciders H4.
Ztac.
uh H8; ee.
au.

ir.
ufi coinciders H4; Ztac.
uh H10.
ee.
ap H12.
am.

uh H1; ee.
Apply H17 with y.
am.

am.

ir.
ufi coinciders H4.
Ztac.
uh H10; ee.
ap H13.
am.

uh H1; ee.
Apply H17 with y.
am.

am.
Save. 




Lemma scale_next : (a,b,c,z:E)(is_ultra_linear_subset a b) -> (downward_saturated a b c) ->
(is_bottom_element a (complement b c) z) ->
(eq_ultra_bound a c z).
ir.
Assert (intersection2 b (punctured_downward_subset a z))==c.
ap extensionality; uf sub; ir.
Apply use_complement with b.
Remind '(intersection2_first H2).
am.

uf not; ir.
Assert (inc x (punctured_downward_subset a z)).
Remind '(intersection2_second H2).
am.

ufi punctured_downward_subset H4; Ztac.
uh H1; ee.
uh H1; ee.
Remind '(H10 ? H3).
Apply no_lt_leq with a x z.
am.

am.

am.

ap intersection2_inc.
uh H0; ee.
ap H4; am.

uf punctured_downward_subset; ap Z_inc.
uh H0; ee.
ap H3.
ap H4; am.

uh H.
ee.
uh H.
ee.
uh H; ee.
uh H6; ee.
Assert (inc x (U (suborder b a))).
rw underlying_suborder.
uh H0; ee.
ap H9; am.

Assert (inc z (U (suborder b a))).
rw underlying_suborder.
uh H1; ee.
uh H1; ee.
rwi inc_complement H9; ee.
am.

Remind '(H7 ? ? H8 H9).
nin H10.
rwi leq_suborder_all H10.
ee.
Remind '(leq_eq_or_lt H H12).
nin H13.
uh H1; ee.
rwi inc_complement H14.
ee.
Assert False.
ap H15.
wr H13.
am.

Elim H16.

am.

am.

am.

rwi leq_suborder_all H10; ee.
uh H0.
ee.
Assert (inc z c).
Apply H15 with x.
am.

am.

am.

uh H1.
ee.
rwi inc_complement H17; ee.
Assert False.
ap H18; am.

Elim H19.

am.

am.

wr H2.
uh H; ee.
ap H3.
uh H1.
ee.
rwi inc_complement H4.
ee.
am.
Save.

Lemma next_eq : (a,b,c,d,x,y:E)(is_ultra_linear_subset a b) -> (is_ultra_linear_subset a c)
-> (downward_saturated a b d) -> (downward_saturated a c d) ->
(is_bottom_element a (complement b d) x) -> (is_bottom_element a (complement c d) y) ->
x==y.
ir.
Remind '(scale_next H H1 H3).
Remind '(scale_next H0 H2 H4).
ufi eq_ultra_bound H5.
ufi eq_ultra_bound H6.
ee.
wr H8; am.
Save.

Lemma next_or : (a,b,c,x,y:E)(is_ultra_linear_subset a b) -> (downward_saturated a b c) ->
(is_bottom_element a (complement b c) x) -> (inc y b) -> (leq a y x) ->
(x==y \/ (inc y c)).
ir.
Assert (axioms a).
uh H.
ee.
uh H; ee.
uh H; ee.
am.

Remind '(leq_eq_or_lt H4 H3).
nin H5.
ap or_introl.
sy; am.

Assert ~x==y->(inc y c).
ir.
Apply use_complement with b.
am.

uf not; ir.
uh H1; ee.
uh H1; ee.
Remind '(H11 y H7).
Assert x==y.
Apply leq_leq_eq with a.
am.

am.

am.

ap H6; am.

ap excluded_middle.
uf not; ir.
ap H7.
ap or_introl.
ap excluded_middle.
uf not; ir.
ap H7.
ap or_intror.
ap H6; am.
Save. 



Lemma next_coincide : (a,b,c,d,x,y:E)(is_ultra_linear_subset a b) -> (is_ultra_linear_subset a c)
-> (downward_saturated a b d) -> (downward_saturated a c d) ->
(is_bottom_element a (complement b d) x) -> (is_bottom_element a (complement c d) y) ->
(coincide_at a b c x).
ir.
Assert x==y.
Apply next_eq with a b c d; am.

uhg.
dj.
ufi is_bottom_element H3; ee.
rwi inc_complement H6; ee.
am.

ufi is_bottom_element H4; ee.
rwi inc_complement H7; ee.
rw H5; am.

Remind '(next_or H H1 H3 H8 H9).
nin H10.
wr H10.
am.

ufi downward_saturated H2; ee.
ap H12; am.

Assert (leq a y0 y).
wr H5.
am.

Remind '(next_or H0 H2 H4 H9 H11).
nin H12.
wr H12.
wr H5; am.

ufi downward_saturated H1; ee.
ap H14.
am.
Save. 


Lemma show_sub_or : (b,c:E)((nonempty (complement b c)) -> (nonempty (complement c b)) -> False) ->
((sub b c) \/ (sub c b)).
Exact
[b,c:E;
 H:((nonempty (complement b c))->(nonempty (complement c b))->False)]
 (excluded_middle
   [H0:((sub b c)\/(sub c b)->False)]
    (H
      (excluded_middle
        [H1:((nonempty (complement b c))->False)]
         (H0
           (or_introl (sub b c) (sub c b)
             [x:E; H2:(inc x b)]
              (excluded_middle
                [H3:((inc x c)->False)]
                 (H1
                   (nonempty_intro
                     (eqT_ind_r Prop (A (inc x b) ~(inc x c)) [P:Prop]P
                       <(inc x b),~(inc x c)>{H2,H3}
                       (inc x (complement b c)) (inc_complement b c x))))))))
      (excluded_middle
        [H1:((nonempty (complement c b))->False)]
         (H0
           (or_intror (sub b c) (sub c b)
             [x:E; H2:(inc x c)]
              (excluded_middle
                [H3:((inc x b)->False)]
                 (H1
                   (nonempty_intro
                     (eqT_ind_r Prop (A (inc x c) ~(inc x b)) [P:Prop]P
                       <(inc x c),~(inc x b)>{H2,H3}
                       (inc x (complement c b)) (inc_complement c b x)))))))))).


Save. 



Lemma wo_subset_choose_bottom : (a,b:E)(is_wo_subset a b) -> (nonempty b) ->
(is_bottom_element a b (choose_bottom_element a b)).
ir.
Assert (exists [x:E](is_bottom_element a b x)).
uh H.
ee.
uh H1; ee.
Assert (sub b (U (suborder b a))).
rw underlying_suborder.
uf sub; ir; am.

Remind '(H2 b H3 H0).
nin H4.
sh x.
uhg.
ee.
uhg; ee.
uh H.
ee; am.

uh H; ee; am.

uh H4; ee.
uh H; ee.
ap H6; am.

ir.
uh H4; ee.
uh H4; ee.
Remind '(H9 y H5).
rwi leq_suborder_all H10; ee.
am.

uh H; ee; am.

uh H; ee; am.

uh H4; ee.
am.

Remind '(choose_pr H1).
Exact H2.
Save. 




Lemma uls_or : (a,b,c:E)(is_ultra_linear_subset a b) -> (is_ultra_linear_subset a c) ->
((sub b c) \/ (sub c b)).
ir.
Pose d:=(coinciders a b c).
Assert (downward_saturated a b d).
uf d; ap coinciders_saturated.


am.

am.

Assert (downward_saturated a c d).
uf d.
Assert (coinciders a b c)==(coinciders a c b).
ap coinciders_symm.

rw H2.
ap coinciders_saturated.

am.

am.

Apply show_sub_or; ir.
Assert (nonempty (complement b d)).
nin H3.
sh y.
rw inc_complement; ee.
rwi inc_complement H3; ee.
am.

uf not; ir.
rwi inc_complement H3; ee.
ap H6.
uh H2; ee.
ap H8; am.

Assert (nonempty (complement c d)).
nin H4.
sh y.
rw inc_complement; ee.
rwi inc_complement H4; ee; am.

uf not; ir.
rwi inc_complement H4; ee.
ap H7.
uh H1; ee.
ap H9.
am.

ufk is_ultra_linear_subset H.
ufk is_ultra_linear_subset H0.
ee.

Assert (is_wo_subset a (complement b d)).
Apply wo_sub with b.
am.

uf sub; ir.
rwi inc_complement H9; ee; am.

Assert (is_wo_subset a (complement c d)).
Apply wo_sub with c.
am.

uf sub; ir.
rwi inc_complement H10; ee; am.

Remind '(wo_sub_bottom H9 H5).
Remind '(wo_sub_bottom H10 H6).
LetTac x:=(choose_bottom_element a (complement b d)).
LetTac y:=(choose_bottom_element a (complement c d)).
Remind '(next_eq X0 X1 H1 H2 H11 H12).
Remind '(next_coincide X0 X1 H1 H2 H11 H12).
Assert (inc x d).
uf d.
uf coinciders.
ap Z_inc.
ufi is_bottom_element H11; ee.
rwi inc_complement H15; ee; am.

am.

ufi is_bottom_element H11.
ee.
rwi inc_complement H16.
ee.
ap H17; am.
Save. 

Lemma uls_sub_downward_saturated : (a,b,c:E; hyp : (sub c b))
(is_ultra_linear_subset a b) -> (is_ultra_linear_subset a c) ->
(downward_saturated a b c). 
ir.
Pose d:=(coinciders a b c).
Assert (downward_saturated a b d).
uf d; ap coinciders_saturated.


am.

am.

Assert (downward_saturated a c d).
uf d.
Assert (coinciders a b c)==(coinciders a c b).
ap coinciders_symm.

rw H2.
ap coinciders_saturated.

am.

am.

Apply excluded_middle; uf not; ir. 
Assert (nonempty (complement b d)). 
Apply excluded_middle; uf not; ir. 
Assert (sub b d). uf sub; ir. 
Apply use_complement with b. am. uf not; ir. ap H4. 
sh x. am. Assert c==d. ap extensionality; uf sub; ir. 
ap H5.
ap hyp. am. ufi downward_saturated H2; ee. ap H8; am. 
ap H3. rw H6. am. 
Assert (nonempty (complement c d)). 
Apply excluded_middle; uf not; ir. 
Assert (sub c d). uf sub; ir. 
Apply use_complement with c. am. uf not; ir.
ap H5; sh x. am. Assert c==d. ap extensionality.
am. ufi downward_saturated H2; ee. am. 
ap H3. rw H7; Exact H1. 



ufk is_ultra_linear_subset H.
ufk is_ultra_linear_subset H0.
ee.

Assert (is_wo_subset a (complement b d)).
Apply wo_sub with b.
am.

uf sub; ir.
rwi inc_complement H8; ee; am.

Assert (is_wo_subset a (complement c d)).
Apply wo_sub with c.
am.

uf sub; ir.
rwi inc_complement H9; ee; am.

Remind '(wo_sub_bottom H8 H4).
Remind '(wo_sub_bottom H9 H5).
LetTac x:=(choose_bottom_element a (complement b d)).
LetTac y:=(choose_bottom_element a (complement c d)).
Remind '(next_eq X0 X1 H1 H2 H10 H11).
Remind '(next_coincide X0 X1 H1 H2 H10 H11).
Assert (inc x d).
uf d.
uf coinciders.
ap Z_inc.
ufi is_bottom_element H10; ee.
rwi inc_complement H14; ee; am.

am.

ufi is_bottom_element H11.
ee.
rwi inc_complement H15.
ee.
ap H16. wr H12.  am.
Save.


Definition increasing_ds_family := [a,f:E]
((x,y:E)(inc x f) -> (inc y f) -> 
((downward_saturated a x y) \/ (downward_saturated a y x))).

Lemma wo_subset_increasing_union : 
(a,f:E)(axioms a) -> (increasing_ds_family a f) -> 
((b:E)(inc b f) -> (is_wo_subset a b)) -> 
(is_wo_subset a (union f)).
ir. uhg. dj. uhg; dj. am. uhg; ir. 
Remind '(union_exists H3). nin H4; ee. Remind '(H1 x0 H5). 
ufi is_wo_subset H6. ee. ufi is_linear_subset H6; ee. 
ap H8; am. uhg; dj. 
ap suborder_axioms. am. am. rwi underlying_suborder H5. 
rwi underlying_suborder H6. 
Remind '(union_exists H5). nin H7. Remind '(union_exists H6). 
nin H8. ee. ufi increasing_ds_family H0. 
Remind '(H0 ? ? H10 H9). nin H11. 
Assert (inc y x0). ufi downward_saturated H11. ee. 
ap H13; am. Remind '(H1 x0 H10). ufi is_wo_subset H13.
ee. ufi is_linear_subset H13; ee. 
ufi is_linear H16; ee. 
Assert (inc x (U (suborder x0 a))). 
rw underlying_suborder. am. 
Assert (inc y (U (suborder x0 a))). 
rw underlying_suborder. am. 
Remind '(H17 x y H18 H19). 
nin H20. ap or_introl. rwi leq_suborder_all H20. 
rw leq_suborder_all. ee; am. 
am. am. am. am. 
ap or_intror. rwi leq_suborder_all H20. 
rw leq_suborder_all. ee; am. 
am. am. am. am. 

Assert (inc x x1). ufi downward_saturated H11. ee. 
ap H13; am. Remind '(H1 x1 H9). ufi is_wo_subset H13.
ee. ufi is_linear_subset H13; ee. 
ufi is_linear H16; ee. 
Assert (inc x (U (suborder x1 a))). 
rw underlying_suborder. am. 
Assert (inc y (U (suborder x1 a))). 
rw underlying_suborder. am. 
Remind '(H17 x y H18 H19). 
nin H20. ap or_introl. rwi leq_suborder_all H20. 
rw leq_suborder_all. ee; am. 
am. am. am. am. 
ap or_intror. rwi leq_suborder_all H20. 
rw leq_suborder_all. ee; am. 
am. am. am. am. 


uhg; dj. ufi is_linear_subset H2; ee. am. 
nin H5. Assert (inc y (union f)). rwi underlying_suborder H4. 
ap H4. am. Remind '(union_exists H6). 
nin H7. ee. Assert (is_wo_subset a x). ap H1; am.
ufi is_wo_subset H9. ee. 
Assert (nonempty (intersection2 b x)). 
sh y. ap intersection2_inc. 
am. am. Pose z := (choose_bottom_element (suborder x a)
(intersection2 b x)). Assert (is_bottom_element
(suborder x a) (intersection2 b x) z). 
uf z. ap wo_choose_bottom. am. 
uf sub; ir. Remind '(intersection2_second H12). 
rw underlying_suborder. am. am. 
sh z. ufi is_bottom_element H12. ee. 
Assert (sub (union f) (U a)). 
uf sub; ir. Remind '(union_exists H14). 
nin H15; ee. Assert (is_wo_subset a x1). 
ap H1; am. ufi is_wo_subset H17; ee. ufi is_linear_subset
H17; ee. ap H19. am. 
uf is_bottom_element; dj. 
ufi is_lower_bound H12; uf is_lower_bound; ee. 
ap suborder_axioms. am. am. am. 
rw underlying_suborder. 
Apply union_inc with x. rwi underlying_suborder H16; am.
am. ir. 
Assert (inc y0 (union f)). rwi underlying_suborder H4.
ap H4; am.
Remind '(union_exists H19). nin H20; ee. 
ufi increasing_ds_family H0. 
Remind '(H0 x x0 H8 H21). nin H22. 
Assert (leq (suborder x a) z y0). 
ap H17. ap intersection2_inc. am. ufi downward_saturated
H22. ee. ap H24; am. rw leq_suborder_all. 
rwi leq_suborder_all H23. ee. Apply union_inc
with x. am. am. Apply union_inc with x. am. 
am. am. am. ufi is_linear_subset H9; ee. am. am. 
am. 
ufi is_linear H3. ee. 
Assert 
(leq (suborder (union f) a) z y0)\/
(leq (suborder (union f) a) y0 z). 
ap H23. rw underlying_suborder. 
Apply union_inc with x. Apply intersection2_second with b. 
am. am. rw underlying_suborder. am. nin H24. 
am. 
Assert (inc z x). Apply intersection2_second with b.
Exact H13. 
Assert (inc y0 x).
ufi downward_saturated H22. ee. Apply H28 with z. 
am. 
am. 
rwi leq_suborder_all H24; ee. am. am. 
am. Assert (leq (suborder x a) z y0). 
ap H17. ap intersection2_inc. am. 
am. 
rw leq_suborder_all; ee. 
Apply union_inc with x. am. am. 
Apply union_inc with x. am. am. 
rwi leq_suborder_all H27; ee. 
am. am. ufi is_linear_subset H9; ee. Exact H28.
am. am. Apply intersection2_first with x.
am. 
Save. 

Lemma uls_increasing_ds : (a,f:E)(axioms a) -> 
((x:E)(inc x f) -> (is_ultra_linear_subset a x)) ->
(increasing_ds_family a f).
ir. uhg. ir. Assert (sub x y) \/ (sub y x).
Apply uls_or with a; ap H0; am.
nin H3. ap or_intror. 
ap uls_sub_downward_saturated. am. 
ap H0; am. ap H0; am. 
ap or_introl. 
ap uls_sub_downward_saturated. am. 
ap H0; am. ap H0; am. 
Save.

Lemma uls_union_downward : (a,f,z:E)(axioms a) -> 
((x:E)(inc x f) -> (is_ultra_linear_subset a x)) ->
(inc z f) -> (downward_saturated a (union f) z). 
ir. uhg. ee. am. uf sub; ir. Remind '(union_exists H2). 
nin H3; ee. Remind '(H0 x0 H4). 
uh H5. ee. uh H5; ee. uh H5; ee. ap H8; am. 
uf sub; ir. Apply union_inc with z. am. 
am. ir. Remind '(union_exists H3).
nin H5. ee. Assert (sub x0 z) \/ (sub z x0).
Apply uls_or with a. ap H0; am. ap H0; am. 
nin H7. ap H7; am. Assert (downward_saturated a x0 z). 
ap uls_sub_downward_saturated. am. ap H0; am. 
ap H0; am. ufi downward_saturated H8. ee. 
Apply H11 with x. am. am. am.  
Save. 

Lemma uls_union_int_rw : (a,b,x,z:E)(axioms a) ->
(downward_saturated a b x) -> (inc z x) -> 
(intersection2 b (punctured_downward_subset a z)) ==
(intersection2 x (punctured_downward_subset a z)).
ir. 
ap extensionality; uf sub; ir;
Remind '(intersection2_first H2); 
Remind '(intersection2_second H2).  
ap intersection2_inc. 
ufi downward_saturated H0; ee. 
Apply H7 with z. am. am. 
ufi punctured_downward_subset H4. Ztac. ufi lt H9; ee. 
am. am. 
ap intersection2_inc. ufi downward_saturated H0; ee. 
ap H6; am. am. 
Save. 

Lemma ultra_linear_subset_union : (a,f:E)(axioms a) -> 
((x:E)(inc x f) -> (is_ultra_linear_subset a x)) ->
(is_ultra_linear_subset a (union f)).
ir. 
Assert (increasing_ds_family a f). 
ap uls_increasing_ds. am. am. 
uhg; dj. 
ap wo_subset_increasing_union. 
am. am. ir. Remind '(H0 b H2). 
ufi is_ultra_linear_subset H3.
ee. am. Remind '(union_exists H3). 
nin H4. ee. Assert (intersection2 (union f)
(punctured_downward_subset a x)) == 
(intersection2 x0 (punctured_downward_subset a x)). 
ap uls_union_int_rw. am. ap uls_union_downward. 
am. Exact H0. am. am. rw H6. 
Remind '(H0 x0 H5). 
ufi is_ultra_linear_subset H7. 
ee. ap H8. am. 
Save.




Lemma wo_subset_new : (a,b,x:E)(is_wo_subset a b) -> 
~(inc x b) ->(is_upper_bound a b x) ->
(is_wo_subset a (union2 b (singleton x))). 
ir. ufk is_wo_subset H. ufk is_upper_bound H1. ee. ufk is_well_ordered H3.
ufk is_linear_subset H. ee. ufk is_linear H8. ee. uhg; dj. uhg; dj. am.
uf sub; ir. Remind '(union2_or H11). nin H12. ap H2. am.
Remind '(singleton_eq H12). rw H13; am. uhg; dj. ap suborder_axioms.
am. am. rwi underlying_suborder H13. rwi underlying_suborder H14.
Remind '(union2_or H13). Remind '(union2_or H14). nin H15. nin H16.
ufi is_linear X4. ee. Assert (leq (suborder b a) x0 y)\/(leq (suborder b a) y x0).
ap H18. rw underlying_suborder; am. rw underlying_suborder; am. nin H19.
ap or_introl. rw leq_suborder_all; ee. am. am. rwi leq_suborder_all H19.
ee. am. am. am. am. am. ap or_intror. rw leq_suborder_all; ee. am.
am. rwi leq_suborder_all H19. ee; am. am. am. am. am. Remind '(singleton_eq H16).
ap or_introl. rw leq_suborder_all; ee. am. am. rw H17.
ap H5. am. am. am. Remind '(singleton_eq H15). ap or_intror. rw leq_suborder_all; ee.
am. am. rw H17. nin H16. ap H5; am. Remind '(singleton_eq H16).
rw H18. ufi axioms H; ee. ap H. am. am. am. uhg. dj. ufi is_linear_subset H10.
ee. am. Apply by_cases with (nonempty (intersection2 b0 b)). ir. ufi is_well_ordered X2.
ee. LetTac b1:=(intersection2 b0 b). Assert (sub b1 (U (suborder b a))). rw underlying_suborder.
uf b1; uf sub; ir. Apply intersection2_second with b0. am. Remind '(H16 b1 H17 H14).
nin H18. sh x0. uhg; dj. uhg; dj. ap suborder_axioms. am. uf sub; ir.
Remind '(union2_or H19). nin H20. ap H2; am. Remind '(singleton_eq H20). rw H21.
am. am. rw underlying_suborder. Apply union2_first. rwi underlying_suborder H17.
ap H17. ufi is_bottom_element H18; ee. am. rw leq_suborder_all.
ee. rwi underlying_suborder H21. Exact H21. rwi underlying_suborder H20. ap H20.
am. Apply by_cases with (inc y b). ir. Assert (inc y b1). uf b1; ap intersection2_inc; am.
ufi is_bottom_element H18; ee. ufi is_lower_bound H18; ee. Remind '(H28 y H24).
rwi leq_suborder_all H29. ee. am. am. am. ir. Assert (inc y (union2 b (singleton x))).
rwi underlying_suborder H20. ap H20. am. Remind '(union2_or H24). nin H25.
Assert False. ap H23; am. Elim H26. Remind '(singleton_eq H25). rw H26.
Assert (inc x0 (union2 b (singleton x))). rwi underlying_suborder H21; Exact H21.
Remind '(union2_or H27). nin H28. ap H5. am. Remind '(singleton_eq H28).
rw H29. ufi axioms H1; ee. ap H1; am. am. uf sub; ir. Remind '(union2_or H23).
nin H24. ap H2; am. Remind '(singleton_eq H24). rw H25; am. ufi is_bottom_element H18.
ee. ufi b1 H20. Apply intersection2_first with b; am. ir. Assert (sub b0 (singleton x)).
uf sub; ir. rwi underlying_suborder H12. Assert (inc x0 (union2 b (singleton x))).
ap H12. am. Remind '(union2_or H16). nin H17. Assert False. ap H14. sh x0.
ap intersection2_inc; am. Elim H18. am. Assert b0==(singleton x). ap extensionality.
am. uf sub; ir. Remind '(singleton_eq H16). rw H17. nin H13. Assert (inc y (singleton x)).
ap H15; am. Remind '(singleton_eq H18). wr H19. am. rw H16. sh x. uhg; dj. uhg; dj.
ap suborder_axioms. am. ufi is_linear_subset H10; ee. am. uf sub; ir. rw underlying_suborder.
ap union2_second. am. rw underlying_suborder. ap union2_second. ap singleton_inc.
Remind '(singleton_eq H20). rw H21. rw leq_suborder_all. dj. ap union2_second; ap singleton_inc.
am. ufi axioms H1; ee; ap H1. am. am. ufi is_linear_subset H10; ee; am. ap singleton_inc.
Save. 

Lemma uls_new : (a,b,x:E)(is_ultra_linear_subset a b) -> 
(eq_ultra_bound a b x) -> (is_ultra_linear_subset a (union2 b (singleton x))). 
ir. uhg; dj. ap wo_subset_new. uh H; ee. am. uh H0; ee. uh H0; ee.
am. uh H0; ee. uh H0; ee. am. Remind '(union2_or H2). nin H3.
Assert (intersection2 (union2 b (singleton x)) (punctured_downward_subset a x0))
==(intersection2 b (punctured_downward_subset a x0)).
ap extensionality; uf sub; ir. Remind '(intersection2_first H4).
Remind '(intersection2_second H4). ap intersection2_inc. Remind '(union2_or H5).
nin H7. am. Remind '(singleton_eq H7). rw H8. ufi punctured_downward_subset H6.
Ztac. uh H0; ee. uh H0; ee. uh H0; ee. Remind '(H15 x0 H3). rwi H8 H10.
Assert False. Apply no_lt_leq with a x x0. am. am. am. Elim H17. am.
Remind '(intersection2_first H4). Remind '(intersection2_second H4).
ap intersection2_inc. ap union2_first. am. am. rw H4. uh H; ee. ap H5.
am. Remind '(singleton_eq H3).
Assert (intersection2 (union2 b (singleton x)) (punctured_downward_subset a x0))==b.
ap extensionality; uf sub; ir. Remind '(intersection2_first H5). Remind '(intersection2_second H5).
Remind '(union2_or H6). nin H8. am. Remind '(singleton_eq H8).
ufi punctured_downward_subset H7. Ztac. ufi lt H11. ee. Assert False.
ap H12. rw H4; am. Elim H13. ap intersection2_inc. ap union2_first; am.
uf punctured_downward_subset; ap Z_inc. uh H; ee. uh H; ee. uh H; ee.
ap H8; am. uh H0; ee. uh H0; ee. uh H0; ee. uf lt; ee. rw H4. ap H10; am.
uf not; ir. ap H7. wr H4. wr H11. am. rw H5. rw H4. am.
Save. 



Definition uls_pool := [a:E](Z (powerset (U a)) [b:E](is_ultra_linear_subset a b)).

Lemma inc_uls_pool_rw : (a,b:E)(inc b (uls_pool a))== (is_ultra_linear_subset a b).
ir. ap iff_eq; ir. ufi uls_pool H. Ztac. uf uls_pool. ap Z_inc.
ap powerset_inc. uh H; ee. uh H; ee. uh H; ee. am. am.
Save.

Definition max_uls := [a:E](union (uls_pool a)).

Lemma uls_sub_uls_pool : (a,b:E)(is_ultra_linear_subset a b) -> (sub b (max_uls a)).
ir. uf sub; ir. uf max_uls. Apply union_inc with b. am. rw inc_uls_pool_rw. am.
Save.

Lemma max_uls_uls : (a:E)(axioms a) -> (is_ultra_linear_subset a (max_uls a)).
ir. uf max_uls. ap ultra_linear_subset_union. am. ir. rwi inc_uls_pool_rw H0. am.
Save. 

Lemma ub_inc_max_uls : (a,b,x:E)(is_ultra_linear_subset a b) -> (eq_ultra_bound a b x) ->
(inc x (max_uls a)).
ir. Assert (sub (union2 b (singleton x)) (max_uls a)). ap uls_sub_uls_pool.
ap uls_new. am. am. ap H1. ap union2_second. ap singleton_inc.
Save. 
 


Lemma no_ultra_zorn : (a:E)~(is_ultra_zorn a).
uf not; ir. uh H; ee. LetTac c:=(max_uls a). Assert (is_ultra_linear_subset a c).
uf c; ap max_uls_uls. am. LetTac x:=(ultra_bound a c). Assert (is_ultra_bound a c x).
uf x. ap H0. uh H1; ee. uh H1; ee. am. ufk is_ultra_bound H2.
ee. ap H3. uf c. Apply ub_inc_max_uls with c. am. uhg; ee. am. tv.
Save.


Lemma zorn : (a:E)(axioms a) -> 
((b:E)(is_linear_subset a b) -> (exists [x:E](is_upper_bound a b x))) ->
(exists [z:E](is_maximal a (U a) z)).
ir. ap excluded_middle. uf not; ir. Apply no_ultra_zorn with a. uhg; dj.
am. Remind '(H0 b H3). Apply by_cases with (exists [y:E](is_ultra_bound a b y)).
ir. Remind '(choose_pr H5). am. ir. Assert False. ap H1. nin H4.
sh x. uhg; dj. am. uf sub; ir; am. uh H4; ee. am. Assert (is_upper_bound a b y).
uhg; ee. am. uh H3; ee. am. am. ir. uh H4; ee. uh H; ee. Apply H18 with x.
ap H14; am. am. ap excluded_middle; uf not; ir. Assert (is_top_element a b x).
uhg; ee. am. ap excluded_middle. uf not; ir. ap H5. sh x. uhg; ee. am.
am. Assert (is_top_element a b y). uhg; ee. am. ap excluded_middle.
uf not; ir. ap H5. sh y. uhg; ee. am. am. Remind '(top_element_unique H13 H14).
ap H12; am. Elim H6.
Save. 

End Zorn. Export Zorn. 

End Order.