proposition: Lemma same_cardinality_transitive : forall A B C, same_cardinality A B -> same_cardinality B C -> same_cardinality A C.
proof: Proof. intros A B C [f [g [HAB1 HAB2]]] [h [k [HBC1 HBC2]]]; repeat (match goal with [id1: forall (_:_), compose _ _ _ _ _ _ = identity _ _ |- _ ]=> unfold compose in id1; unfold identity in id1 end); exists (compose _ _ _ h f); exists (compose _ _ _ g k); unfold compose; unfold identity; split; [ intro c; rewrite (HAB1 (k c)) | intro a; rewrite (HBC2 (f a)) ]; trivial. Defined.