proposition: Lemma suborder_wo_avatar_decreasing : forall u a x, is_well_ordered a -> sub u (U a) -> inc x u -> ordinal_leq (wo_avatar (suborder u a) x) (wo_avatar a x).
proof: Proof. ir. set (b:=suborder u a). assert (lem1: U b = u). uf b; rw underlying_suborder; tv. assert (lem2 : is_well_ordered b). uf b; ap suborder_well_ordered. am. am. util (wo_induction lem2 (p:= fun y=> (ordinal_leq (wo_avatar b y) (wo_avatar a y)))). ir. uhg; ee. ap wo_avatar_is_ordinal. am. am. ap wo_avatar_is_ordinal. am. ap H0. wr lem1; am. uhg; ir. wri wo_punctured_downward H4. rwi Image.inc_rw H4. nin H4. ee. ufi punctured_downward_subset H4. Ztac. cp (H3 _ H6 H7). rwi H5 H8. assert (lt a x2 x0). uh H7. uhg; ee; try am. ufi b H7. rwi leq_suborder_all H7. ee. am. lu. am. assert (ordinal_lt x1 (wo_avatar a x0)). uhg; ee. uhg; ee. uh H8; ee; am. ap wo_avatar_is_ordinal. am. ap H0. wr lem1; am. apply sub_trans with (wo_avatar a x2). uh H8; ee; am. uh H9; ee. rwi wo_leq_rw H9. lu. am. ap H0; wr lem1; am. lu. uhg; ir. rwi wo_lt_rw H9. uh H9; ee. ap H11. ap extensionality. lu. wr H10. lu. am. ap H0; wr lem1; am. ap H0; wr lem1; am. rwi ordinal_lt_rw H10. ee; am. am. am. wri lem1 H1. cp (H2 _ H1). am. Qed.
imports: Arith transfinite