proposition: Lemma wo_ordinal_cardinal_leq : forall a, is_well_ordered a -> ordinal_leq (cardinality (U a)) (wo_ordinal a).
proof: Proof. ir. ap cardinality_smallest. ap wo_ordinal_is_ordinal. am. ap wo_ordinal_isomorphic; am. Qed.
imports: Arith ordinal