proposition: Lemma ntrans_hcompose : forall a b x, hcomposable a b -> ob (osource b) x -> ntrans (hcompose a b) x = comp (otarget a) (ntrans a (fob (target b) x)) (fmor (source a) (ntrans b x)).
proof: Proof. ir. uf hcompose. rw ntrans_vcompose. rw otarget_htrans_right. rw ntrans_htrans_right. rw ntrans_htrans_left. tv. am. uh H; ee. nw. rww osource_htrans_left. Qed.
imports: Arith functor