proposition: Lemma wo_same_order : forall a b : E, same_order a b -> is_well_ordered a -> is_well_ordered b.
proof: Proof. ir. uhg; dj. uhg; dj. ufi same_order H; ee. ufi is_suborder H; ee. am. assert (leq b x y = leq a x y). sy; ap same_leq_eq. am. assert (leq b y x = leq a y x). sy; ap same_leq_eq; am. rw H4. rw H5. uh H0. ee. uh H0; ee. ap H7. assert (U a = U b). ap same_underlying. am. rw H8; am. assert (U a = U b). ap same_underlying; am. rw H8; am. assert (U a = U b). ap same_underlying; am. assert (sub b0 (U a)). rw H4; am. uh H0; ee. cp (H6 _ H5 H3). nin H7. sh x. uhg; ee. uhg; ee. uh H; ee. ufi is_suborder H; ee. am. am. uh H7; ee. ap H2; am. ir. assert (leq b x y = leq a x y). sy. ap same_leq_eq. am. rw H9. uh H7. ee. uh H7. ee. ap H13. am. uh H7. ee. am. Qed.
imports: universe