proposition: Lemma are_isomorphic_symm : forall x y, are_isomorphic x y -> are_isomorphic y x.
proof: Proof. ir. rwi iso_isotrans_rw H. uhg. sh (Function.create y (Transformation.inverse x (isotrans x y))). wr trans_map_bijective. apply Transformation.inverse_bijective with (isotrans x y). apply are_inverse_symm. apply Transformation.bijective_inverse. am. Qed.
imports: set_theory