proposition: Lemma new_order_wo : forall a y:E, ~inc y (U a) -> is_well_ordered a -> (is_well_ordered (create (tack_on (U a) y) (new_order a y))).
proof: Proof. ir. set (b:= (create (tack_on (U a) y) (new_order a y))). assert (U b = tack_on (U a) y). uf b; rw underlying_create; tv. assert (forall u :E,inc u (U b) -> (inc u (U a) \/ u = y)). ir. rwi H1 H2. cp (tack_on_or H2). am. assert (forall u v:E, leq b u v = (leq a u v \/ (v = y & (inc u (U b))))). ir. ap iff_eq; ir. ufi b H3. rwi leq_create_all H3; ee. uh H5. nin H5. ap or_introl; am. ap or_intror; ee. am. rw H1; am. uf b; rw leq_create_all; dj. nin H3. rw tack_on_inc. ap or_introl; uh H3; ee; am. ee. rwi H1 H4. am. nin H3. rw tack_on_inc; ap or_introl; uh H3; ee; am. ee. rw tack_on_inc; ap or_intror; am. uhg. nin H3. ap or_introl; am. ee; ap or_intror; am. uhg; dj. uhg; dj. uhg; ee; ir. rw H3. nin (H2 _ H4). ap or_introl; ap leq_refl; try am. do 2 (uh H0; ee); am. ap or_intror; ee; am. rwi H3 H4. nin H4. rw H1. rw tack_on_inc. ap or_introl; uh H4; ee; am. ee; am. uh H4; ee; am. rwi H3 H4. rwi H3 H5. nin H4. nin H5. apply leq_leq_eq with a. do 2 (uh H0; ee); am. am. am. assert False. ap H. ee. wr H5; uh H4; ee; am. elim H6. nin H5. assert False. ap H. ee. wr H4. uh H5; ee; am. elim H6. ee. rw H5; rw H4; tv. rwi H3 H4. rwi H3 H5. nin H4. nin H5. rw H3; ap or_introl. apply leq_trans with y0; try am. do 2 (uh H0; ee); am. ee. rw H3. ap or_intror. ee; try am. rw H1; rw tack_on_inc; ap or_introl. uh H4; ee; am. nin H5; ee. rw H3. assert False. ap H. wr H4; uh H5; ee; am. elim H7. rw H3; ap or_intror; ee; am. cp (H2 _ H5); cp (H2 _ H6). nin H7; nin H8. uh H0; ee. uh H0; ee. cp (H10 _ _ H7 H8). nin H11. ap or_introl. rw H3; ap or_introl; am. ap or_intror. rw H3; ap or_introl; am. ap or_introl; rw H3; ap or_intror. ee; am. ap or_intror; rw H3; ap or_intror. ee; am. ap or_introl; rw H3; ap or_intror; ee; am. set (c:= intersection2 b0 (U a)). assert (sub c b0). uhg; ir. ufi c H7. cp (intersection2_first H7). am. assert (sub c (U a)). uhg; ir. cp (intersection2_second H8); am. apply by_cases with (nonempty c); ir. uh H0; ee. cp (H10 c H8 H9). nin H11. sh x. uhg; ee. uhg; ee. uh H4; ee; am. am. uh H11; ee. ap H5; ap H7; am. ir. assert (inc y0 (U b)). ap H5; am. cp (H2 _ H13). nin H14. rw H3; ap or_introl. uh H11; ee. uh H11; ee. ap H18. uf c; ap intersection2_inc. am. am. rw H3; ap or_intror. ee; try am. uh H11; ee. ap H5; ap H7; am. ap H7; uh H11; ee; am. assert (forall u:E, inc u b0 = (u = y)). ir. ap iff_eq; ir. assert (inc u (U b)). ap H5; am. cp (H2 _ H11). nin H12. assert False. ap H9. sh u. uf c; ap intersection2_inc. am. am. elim H13. am. nin H6. assert (inc y0 (U b)). ap H5; am. nin (H2 _ H11). assert False. ap H9. sh y0. uf c; ap intersection2_inc. am. am. elim H13. rw H10; wr H12; am. sh y. uhg. ee. uhg; ee. uh H4; ee; am. am. rw H1; rw tack_on_inc; ap or_intror; tv. ir. rwi H10 H11. rw H11. rw H3. ap or_intror; ee; tv. rw H1; rw tack_on_inc; ap or_intror; tv. nin H6. rw H10; tv. Qed.
imports: Arith order