proposition: Lemma is_subcategory_trans : forall a b c, is_subcategory a b -> is_subcategory b c -> is_subcategory a c.
proof: Proof. ir. uh H; uh H0; ee. uhg; ee; try am; try tv. transitivity (structure b); try am; try (sy; am). ir. au. ir. au. ir. rww H11. rww H5. au. au. ir. rww H12. rww H6. au. Qed.
imports: Arith ordinal nat_trans