proposition: Lemma punctured_downward_scale : forall a x : E, is_well_ordered a -> inc x (U a) -> scale_subset (punctured_downward_subset a x) a.
proof: Proof. ir. uhg; dj. am. uf punctured_downward_subset. uhg; ir. Ztac. uf punctured_downward_subset. ap Z_inc. uh H4; xd. ufi punctured_downward_subset H3. Ztac. apply leq_lt_trans with y. uh H; ee; uh H; ee; am. am. am. Qed.
imports: Arith order