proposition: Lemma comp_from_arrows : forall u v, is_mor from_arrows u -> is_mor from_arrows v -> source u = target v -> comp from_arrows u v = comps u v.
proof: Proof. ir. uf from_arrows. rw comp_create. tv. rwi is_mor_from_arrows2 H; am. rwi is_mor_from_arrows2 H0; am. am. Qed.
imports: Arith ordinal nat_trans