proposition: Lemma scale_next : forall a b c z : E, is_ultra_linear_subset a b -> downward_saturated a b c -> is_bottom_element a (complement b c) z -> eq_ultra_bound a c z.
proof: Proof. ir. assert (intersection2 b (punctured_downward_subset a z) = c). ap extensionality; uf sub; ir. apply use_complement with b. cp (intersection2_first H2). am. uf not; ir. assert (inc x (punctured_downward_subset a z)). cp (intersection2_second H2). am. ufi punctured_downward_subset H4; Ztac. uh H1; ee. uh H1; ee. cp (H10 _ H3). apply no_lt_leq with a x z. am. am. am. ap intersection2_inc. uh H0; ee. ap H4; am. uf punctured_downward_subset; ap Z_inc. uh H0; ee. ap H3. ap H4; am. uh H. ee. uh H. ee. uh H; ee. uh H6; ee. assert (inc x (U (suborder b a))). rw underlying_suborder. uh H0; ee. ap H9; am. assert (inc z (U (suborder b a))). rw underlying_suborder. uh H1; ee. uh H1; ee. rwi inc_complement H9; ee. am. cp (H7 _ _ H8 H9). nin H10. rwi leq_suborder_all H10. ee. cp (leq_eq_or_lt H H12). nin H13. uh H1; ee. rwi inc_complement H14. ee. assert False. ap H15. wr H13. am. elim H16. am. am. am. rwi leq_suborder_all H10; ee. uh H0. ee. assert (inc z c). apply H15 with x. am. am. am. uh H1. ee. rwi inc_complement H17; ee. assert False. ap H18; am. elim H19. am. am. wr H2. uh H; ee. ap H3. uh H1. ee. rwi inc_complement H4. ee. am. Qed.
imports: universe