proposition: Lemma scale_is_punctured_downward : forall a y : E, scale_subset y a -> strict_sub y (U a) -> punctured_downward_subset a (next a y)= y.
proof: Proof. ir. symmetry. ap extensionality; uhg; ir. uf punctured_downward_subset; ap Z_inc. uh H0; ee. ap H2. am. assert (inc x (U a)). uh H0; ee. ap H2; am. assert (inc (next a y) (U a)). ap next_inc_U. am. uh H; ee. am. uhg; ee. uh H; ee. uh H; ee. uh H; ee. cp (H7 _ _ H2 H3). nin H8. am. assert (inc (next a y) y). apply H5 with x. am. am. assert False. apply next_not_inc with a y. am. uhg; xd. uhg; xd. am. elim H10. uhg; ir. apply next_not_inc with a y. am. uh H; xd. wr H4; am. ap excluded_middle. uhg; ir. assert (leq a (next a y) x). ap next_smallest. am. uh H; xd. ufi punctured_downward_subset H1. Ztac. am. ufi punctured_downward_subset H1; Ztac. uh H5; xd. ap H6. uh H; ee; uh H; ee. uh H; ee. uh H; ee. apply H13. am. am. Qed.
imports: Arith order