proposition: Lemma next_coincide : forall 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.
proof: Proof. 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. cp (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. cp (next_or H0 H2 H4 H9 H11). nin H12. wr H12. wr H5; am. ufi downward_saturated H1; ee. ap H14. am. Qed.
imports: universe