proposition: Lemma uls_or : forall a b c : E, is_ultra_linear_subset a b -> is_ultra_linear_subset a c -> sub b c \/ sub c b.
proof: Proof. ir. set (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. cp (wo_sub_bottom H9 H5). cp (wo_sub_bottom H10 H6). set (x := choose_bottom_element a (complement b d)) in *. set (y := choose_bottom_element a (complement c d)) in *. cp (next_eq X0 X1 H1 H2 H11 H12). cp (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. Qed.
imports: universe