proposition: Lemma ordinal_leq_subset_wo_ordinal : forall a u, is_well_ordered a -> sub u (U a) -> ordinal_leq (cardinality u) (wo_ordinal a).
proof: Proof. ir. ap ordinal_leq_trans. pose (b:=suborder u a). sh (wo_ordinal b). assert (u = (U b)). uf b; rw underlying_suborder. tv. ee. rw H1. uf b. ap wo_ordinal_cardinal_leq. ap suborder_well_ordered. am. am. uf b. ap suborder_wo_ordinal_decreasing. am. am. Qed.
imports: Arith ordinal