proposition: Lemma hcomposable_commutativity : forall a b x, hcomposable a b -> ob (osource b) x -> comp (otarget a) (ntrans a (fob (target b) x)) (fmor (source a) (ntrans b x)) = comp (otarget a) (fmor (target a) (ntrans b x)) (ntrans a (fob (source b) x)).
proof: Proof. ir. cp H. uh H; ee. assert (lem1 : fob (target b) x = target (ntrans b x)). rw target_ntrans. tv. am. am. assert (lem2 : fob (source b) x = source (ntrans b x)). rw source_ntrans. tv. am. am. rw lem1. rw carre. rw lem2. tv. am. ap mor_ntrans. am. am. am. Qed.
imports: Arith functor