proposition: Lemma suborder_wo_ordinal_decreasing : forall u a, is_well_ordered a -> sub u (U a)-> ordinal_leq (wo_ordinal (suborder u a)) (wo_ordinal a).
proof: Proof. ir. uhg; ee. ap wo_ordinal_is_ordinal. ap suborder_well_ordered; am. ap wo_ordinal_is_ordinal; am. uhg; ir. ufi wo_ordinal H1. rwi Image.inc_rw H1. nin H1. ee. wr H2. apply ordinal_saturated with (wo_avatar a x0). ap wo_ordinal_is_ordinal. am. ap wo_avatar_ordinal_inc. am. ap H0. rwi underlying_suborder H1. am. ap suborder_wo_avatar_decreasing. am. am. rwi underlying_suborder H1. am. Qed.
imports: Arith transfinite