proposition: Lemma comp_subcategory : forall a obp morp u v, subcategory_property a obp morp -> mor a u -> mor a v -> source u = target v -> morp u -> morp v -> comp (subcategory a obp morp) u v = comp a u v.
proof: Proof. ir. uf subcategory. rw comp_create. tv. Ztac. app mor_is_mor. Ztac. app mor_is_mor. am. Qed.
imports: Arith ordinal nat_trans