proposition: Lemma next_compatible_lt : forall a y u:E, scale_subset y a -> strict_sub y (U a) -> inc u y -> lt a u (next a y).
proof: Proof. ir. cp (scale_is_punctured_downward H H0). wri H2 H1. ufi punctured_downward_subset H1. Ztac. Qed.
imports: Arith order