proposition: Lemma suborder_well_ordered : forall a b : E, sub a (U b) -> is_well_ordered b -> is_well_ordered (suborder a b).
proof: Proof. ir. ufk is_well_ordered H0; ee. ufk is_linear H0; ee. uf is_well_ordered; dj. uf is_linear; dj. ap suborder_axioms; am. rw leq_suborder_all. rw leq_suborder_all. cp (H2 x y). lapply H6. ir. lapply H7; ir. nin H8. ap or_introl. ee. rwi underlying_suborder H4. exact H4. rwi underlying_suborder H5; ap H5. am. ap or_intror. ee. rwi underlying_suborder H5; ap H5. rwi underlying_suborder H4; ap H4. am. ap H. rwi underlying_suborder H5; ap H5. ap H. rwi underlying_suborder H4; ap H4. am. am. am. am. assert (sub b0 (U b)). uf sub; ir; ap H. rwi underlying_suborder H4; ap H4. am. cp (H1 b0 H6 H5). nin H7. sh x. uf is_bottom_element; dj. uf is_lower_bound; dj. ap suborder_axioms. am. am. am. ap H9. ufi is_bottom_element H7; ee. am. rw leq_suborder_all; dj. rwi underlying_suborder H9. ap H9. ufi is_bottom_element H7; ee. am. rwi underlying_suborder H9; ap H9; am. ufi is_bottom_element H7; ee. ufi is_lower_bound H7; ee. ap H17. am. am. am. ufi is_bottom_element H7; ee; am. Qed.
imports: universe