proposition: Lemma next_smallest : forall a y u:E, strict_sub y (U a) -> is_well_ordered a -> inc u (U a) -> ~ inc u y -> leq a (next a y) u.
proof: Proof. ir. cp (next_bottom_element H H0). uh H1; ee. uh H3; ee. uh H3; ee. ap H7. rw inc_complement; ee. am. am. Qed.
imports: Arith order