proposition: Lemma scale_bicompatible_next : forall (f:E1) (a b y : E), scale_bisubset a b y -> strict_sub y (U a) -> strict_sub y (U b) -> next_compatible f a -> next_compatible f b -> scale_bisubset a b (tack_on y (f y)).
proof: Proof. ir. uhg. dj. uh H; ee. am. uh H; ee; am. assert (f y = next a y). uh H2; ee. uh H; ee. cp (scale_is_punctured_downward H8 H0). wr H11. rw H6. wr next_punctured_downward. trivial. am. ap next_inc_U. am. am. ap next_inc_U. am. am. rw H6. ap scale_subset_next. uh H; xd. am. assert (f y = next b y). uh H; ee. uh H; ee. assert (strict_sub y (U b)). am. cp (scale_is_punctured_downward H9 H12). wr H13. uh H3; ee. rw H14. wr next_punctured_downward. trivial. am. ap next_inc_U. am. am. ap next_inc_U. am. am. rw H7. ap scale_subset_next. uh H; xd. am. cp (tack_on_or H8). cp (tack_on_or H9). nin H10. nin H11. uh H; ee. ap H15. am. am. assert (v = next a y). rw H11; sy. ap next_compatible_scale. am. uh H; ee; am. am. assert (v = next b y). rw H11; sy. ap next_compatible_scale. am. uh H; ee; am. am. assert (lt a u v). rw H12. ap next_compatible_lt. uh H; ee; am. am. am. assert (lt b u v). rw H13. ap next_compatible_lt. uh H; ee; am. am. am. ap iff_eq. ir. uh H15; xd. ir; uh H14; xd. nin H11. assert (u = next a y). rw H10; sy. ap next_compatible_scale. am. uh H; ee; am. am. assert (u = next b y). rw H10; sy. ap next_compatible_scale. am. uh H; ee; am. am. assert (lt a v u). rw H12. ap next_compatible_lt. uh H; ee; am. am. am. assert (lt b v u). rw H13. ap next_compatible_lt. uh H; ee; am. am. am. ap iff_eq. ir. assert False. apply no_lt_leq with a v u. uh H4; ee; uh H4; ee; am. am. am. elim H17. ir. assert False. apply no_lt_leq with b v u. uh H5; ee; uh H5; ee; am. am. am. elim H17. assert (u = v). transitivity (f y). am. sy; am. rw H12. ap iff_eq; ir. ap leq_refl. uh H5; ee; uh H5; ee; am. assert (v = next b y). rw H11. sy; ap next_compatible_scale. am. uh H; ee; am. am. rw H14. ap next_inc_U. am. am. ap leq_refl. uh H4; ee; uh H4; ee; am. assert (v = next a y). rw H11. sy; ap next_compatible_scale. am. uh H; ee; am. am. rw H14; ap next_inc_U; am. Qed.
imports: Arith order