proposition: Lemma vcompose_oppnt' : forall u v, Nat_Trans.axioms u -> Nat_Trans.axioms v -> source u = target v -> vcompose (oppnt' v) (oppnt' u) = oppnt' (vcompose u v).
proof: Proof. ir. assert (axioms (oppnt' u)). app oppnt'_axioms. assert (axioms (oppnt' v)). app oppnt'_axioms. assert (source (oppnt' v) = target (oppnt' u)). rw source_oppnt'. rw target_oppnt'. rww H1. assert (lem1 : otarget u = otarget v). uf otarget. wr H1. rww target_source. assert (lem2 : osource u = osource v). uf osource. rw H1. rww source_target. ap axioms_extensionality. rww vcompose_axioms. ap oppnt'_axioms. rww vcompose_axioms. rw source_vcompose. rw source_oppnt'. rw source_oppnt'. rw target_vcompose. tv. rw target_vcompose. rw target_oppnt'. rw target_oppnt'. rww source_vcompose. ir. rwi osource_vcompose H5. cp H5. rwi osource_oppnt' H6. rwi ob_opp H6. rw ntrans_vcompose. rw otarget_oppnt'. rw ntrans_oppnt'. rw ntrans_oppnt'. rw ntrans_oppnt'. rw comp_opp. ap uneq. rw flip_flip. rw flip_flip. rw ntrans_vcompose. rww lem1. wrr lem2. rww mor_opp. rw flip_flip. ap mor_ntrans. am. wrr lem2. tv. rww mor_opp. rw flip_flip. ap mor_ntrans. am. am. tv. sy; am. rw source_flip. rw target_flip. rw target_ntrans. rw source_ntrans. rww H1. am. am. am. wrr lem2. apply mor_arrow_like with (otarget u). app mor_ntrans. apply mor_arrow_like with (otarget u). app mor_ntrans. wrr lem2. rww vcompose_axioms. rw osource_vcompose. wrr lem2. am. am. am. wrr lem2. am. am. am. Qed.
imports: Arith functor