proposition: Lemma scale_subset_next : forall a y : E, scale_subset y a -> strict_sub y (U a) -> scale_subset (tack_on y (next a y)) a.
proof: Proof. ir. uhg; dj. uh H; xd. uhg; ir. cp (tack_on_or H2). nin H3. uh H; xd. uh H; ee. rw H3; ap next_inc_U; am. cp (tack_on_or H3). nin H5. uh H; ee. rw tack_on_inc. ap or_introl. apply H7 with y0. am. am. rw tack_on_inc. apply by_cases with (inc x y). ir. ap or_introl; am. ir. ap or_intror. assert (leq a (next a y) x). ap next_smallest. am. am. uh H4; xd. am. apply leq_leq_eq with a. uh H; ee. uh H; ee. uh H. ee. am. wr H5; am. am. Qed.
imports: Arith order