proposition: Lemma uls_sub_downward_saturated : forall (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.
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 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. cp (wo_sub_bottom H8 H4). cp (wo_sub_bottom H9 H5). 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 H10 H11). cp (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. Qed.
imports: universe