proposition: Lemma iso_isotrans_rw : forall x y, are_isomorphic x y = Transformation.bijective x y (isotrans x y).
proof: Proof. ir; ap iff_eq; ir. ap isotrans_bij; am. uhg. sh (Function.create x (isotrans x y)). wr trans_map_bijective. am. Qed.
imports: set_theory