proposition: Lemma uls_new : forall 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)).
proof: Proof. 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. cp (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. cp (intersection2_first H4). cp (intersection2_second H4). ap intersection2_inc. cp (union2_or H5). nin H7. am. cp (singleton_eq H7). rw H8. ufi punctured_downward_subset H6. Ztac. uh H0; ee. uh H0; ee. uh H0; ee. cp (H15 x0 H3). rwi H8 H10. assert False. apply no_lt_leq with a x x0. am. am. am. elim H17. am. cp (intersection2_first H4). cp (intersection2_second H4). ap intersection2_inc. ap union2_first. am. am. rw H4. uh H; ee. ap H5. am. cp (singleton_eq H3). assert (intersection2 (union2 b (singleton x)) (punctured_downward_subset a x0) = b). ap extensionality; uf sub; ir. cp (intersection2_first H5). cp (intersection2_second H5). cp (union2_or H6). nin H8. am. cp (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. Qed.
imports: universe