proposition: Lemma iso_sub_trans_rw : forall x y, iso_sub x y = (exists f, Transformation.injective x y f).
proof: Proof. ir. ap iff_eq; ir. uh H; nin H. ee. sh (isotrans x x0). rwi iso_isotrans_rw H. uh H; ee. cp (subidentity_injective H0). cp (compose_injective H2 H3). am. uhg. nin H. sh (Image.create x x0). ee. rw iso_trans_ex_rw. sh x0. apply trans_sub_bijective with x y. am. ap sub_refl. uhg; ir. rwi Image.inc_rw H0. nin H0. ee. wr H1. uh H. ee. uh H. ap H. am. Qed.
imports: Arith ordinal