proposition: Lemma wo_sub_bottom : forall a b : E, is_wo_subset a b -> nonempty b -> is_bottom_element a b (choose_bottom_element a b).
proof: Proof. ir. assert (ex (fun x : E => is_bottom_element a b x)). uh H; ee. set (y := choose_bottom_element (suborder b a) b). assert (is_bottom_element (suborder b a) b y). uf y. ap wo_choose_bottom. am. rw underlying_suborder. uf sub; ir; am. am. sh y. uh H2. ee. uh H2; ee. uhg. ee. uhg; ee. uh H; ee. am. uh H; ee. am. uh H; ee. ap H7; am. ir. cp (H6 _ H7). rwi leq_suborder_all H8; ee. am. uh H; ee; am. uh H; ee; am. am. cp (choose_pr H1). exact H2. Qed.
imports: universe