proposition: Lemma iso_sub_cardinal_leq : forall x y, iso_sub x y -> (ordinal_leq (cardinality x) (cardinality y)).
proof: Proof. ir. assert (iso_sub x (cardinality y)). cp (card_isomorphic y). cp (isomorphic_iso_sub H0). ap iso_sub_trans. sh y; ee; am. ap iso_sub_ordinal_leq. ap cardinality_ordinal. am. Qed.
imports: Arith ordinal