proposition: Lemma iso_sub_trans : forall a c, (exists b, iso_sub a b & iso_sub b c) -> iso_sub a c.
proof: Proof. ir. nin H. ee. rwi iso_sub_trans_rw H0. nin H0. rwi iso_sub_trans_rw H. nin H. rw iso_sub_trans_rw. sh (fun y => (x0 (x1 y))). apply compose_injective with x. am. am. Qed.
imports: Arith ordinal