proposition: Lemma vcompose_point_trans : forall a b u v, composable a u v -> Category.axioms b -> vcompose (point_trans a b u) (point_trans a b v) = point_trans a b (comp a u v).
proof: Proof. ir. rwi composable_facts_rw H; uh H; ee. ap Nat_Trans.axioms_extensionality. rw vcompose_axioms. tv. ap point_trans_axioms. am. am. ap point_trans_axioms; am. rw source_point_trans. rw target_point_trans. rw H5; tv. ap point_trans_axioms. am. am. rw source_vcompose. rw source_point_trans. rw source_point_trans. rw source_comp. tv. am. am. am. rw target_vcompose. rw target_point_trans. rw target_point_trans. rw target_comp. tv. am. am. am. ir. rwi osource_vcompose H8. rwi osource_point_trans H8. rwi ob_functor_cat H8. rw ntrans_vcompose. rw otarget_point_trans. rw ntrans_point_trans. rw ntrans_point_trans. rw ntrans_point_trans. uh H8; ee. wr H10. rw comp_fmor. rww H9. am. rww H9. rww H9. am. am. rww ob_functor_cat. am. rww ob_functor_cat. am. rww ob_functor_cat. rww osource_point_trans. rww ob_functor_cat. am. am. Qed.
imports: Arith nat_trans