proposition: Lemma are_isomorphic_trans : forall x z, (exists y, (are_isomorphic x y & are_isomorphic y z)) -> are_isomorphic x z.
proof: Proof. ir. nin H. ee. rwi iso_isotrans_rw H. rwi iso_isotrans_rw H0. rw iso_trans_ex_rw. sh (fun a => (isotrans x0 z (isotrans x x0 a))). apply compose_bijective with x0. am. am. Qed.
imports: set_theory