proposition: Lemma next_bottom_element : forall a y:E, strict_sub y (U a) -> is_well_ordered a -> is_bottom_element a (complement (U a) y) (next a y).
proof: Proof. ir. uh H0; ee. assert (nonempty (complement (U a) y)). ap strict_sub_nonempty_complement. am. uh H; ee. assert (sub (complement (U a) y) (U a)). ap sub_complement. cp (H1 _ H4 H2). cp (choose_pr H5). cbv beta in H6. uf next. am. Qed.
imports: Arith order