proposition: Lemma wo_ordinal_is_ordinal : forall a, is_well_ordered a -> is_ordinal (wo_ordinal a).
proof: Proof. ir. uf wo_ordinal. uhg. uf wo_avatar. ap lgs_avatar_image. apply scale_subset_is_leq_gen_scale with a. ap next_compatible_next. am. uhg; ee; try am. ap sub_refl. ir. uh H1; ee; am. Qed.
imports: Arith transfinite