proposition: Lemma cardinality_invariant : forall x y, are_isomorphic x y -> cardinality x = cardinality y.
proof: Proof. ir. ap ordinal_leq_leq_eq. ap cardinality_smallest. ap cardinality_ordinal. ap are_isomorphic_trans. sh y. ee; try am. ap card_isomorphic. ap cardinality_smallest. ap cardinality_ordinal. ap are_isomorphic_trans. sh x. ee; try am. ap are_isomorphic_symm. am. ap card_isomorphic. Qed.
imports: Arith ordinal