proposition: Lemma next_punctured_downward : forall a x : E, is_well_ordered a -> inc x (U a) -> x = next a (punctured_downward_subset a x).
proof: Proof. ir. set (y:= punctured_downward_subset a x). apply leq_leq_eq with a. uh H; ee; uh H; ee; am. ap excluded_middle; uhg; ir. assert (lt a (next a y) x). ap excluded_middle; uhg; ir. ap H1. ap linear_not_lt_leq. uh H; ee. am. ap next_inc_U. uf y; ap punctured_downward_strict_sub. uh H; ee; uh H; ee; am. am. am. am. am. assert (inc (next a y) (punctured_downward_subset a x)). uf punctured_downward_subset. ap Z_inc. ap next_inc_U. uf y; ap punctured_downward_strict_sub. uh H; ee; uh H; ee; am. am. am. am. generalize H3. fold y. ap next_not_inc. uf y; ap punctured_downward_strict_sub. uh H; ee; uh H; ee; am. am. am. ap next_smallest. uf y; ap punctured_downward_strict_sub. uh H; ee; uh H; ee; am. am. am. am. uhg; ir. ufi y H1. ufi punctured_downward_subset H1. Ztac. uh H3; xd. Qed.
imports: Arith order