proposition: Lemma next_compatible_scale : forall (f:E1) (a y:E), next_compatible f a -> scale_subset y a -> strict_sub y (U a) -> next a y = f y.
proof: Proof. ir. uh H; ee. assert (inc (next a y) (U a)). ap next_inc_U. am. am. cp (H2 _ H3). wr H4. rw scale_is_punctured_downward. tv. am. am. Qed.
imports: Arith order