proposition: Lemma interchange : forall a b c d, target a = source c -> target b = source d -> osource b = otarget a -> axioms a -> axioms b -> axioms c -> axioms d -> vcompose (hcompose d c) (hcompose b a) = hcompose (vcompose d b) (vcompose c a).
proof: Proof. ir. assert (lema : osource d = otarget c). uf osource. wr target_source. wr H0. wr H. rw source_target. am. am. am. assert (lemb : osource d = osource b). rw lema. wr source_target. rw H0. sy; am. am. assert (lem1 : hcomposable d c). uhg; ee; try am. assert (lem2 : hcomposable b a). uhg; ee; try am. assert (lem5: otarget d = otarget b). uf otarget. rw H0. rw target_source. tv. am. assert (lem6 : osource c = osource a). uf osource. wr H. rw source_target. tv. am. assert (lem7 : otarget d = otarget b). uf otarget. rw H0. rw target_source. tv. am. assert (lem8 : osource b = otarget c). wr lema. sy; am. ap axioms_extensionality. rw vcompose_axioms. tv. ap hcompose_axioms; am. ap hcompose_axioms; am. rw source_hcompose. rw target_hcompose. rw H0. rw H. tv. ap hcompose_axioms. rww vcompose_axioms. sy; am. rww vcompose_axioms. sy; am. rw osource_vcompose. rww otarget_vcompose. rw source_vcompose. rw source_hcompose. rw source_hcompose. rw source_vcompose. rw source_vcompose. tv. rw target_vcompose. rw target_hcompose. rw target_hcompose. rw target_vcompose. rww target_vcompose. ir. rwi osource_vcompose H6. rwi osource_hcompose H6. cp H6. wri lem6 H7. rww ntrans_vcompose. rww ntrans_hcompose. rww ntrans_hcompose. rw ntrans_hcompose. rw ntrans_vcompose. rw otarget_hcompose. rw otarget_vcompose. rw target_vcompose. rw source_vcompose. rw ntrans_vcompose. rww assoc. rww assoc. app uncomp. wrr assoc. wr lema. assert (osource d = source (source b)). nw. rw H8. wr comp_fmor. wr assoc. ap uncomp. tv. rw target_source. wr H0. rw H. sy. ap hcomposable_commutativity. uhg; ee. am. am. am. am. am. nw. nw. fw. nw. nw. fw. nw. nw. nw. fw. nw. nw. nw. nw. rw target_fmor. rw target_ntrans. tv. am. am. nw. nw. fw. nw. nw. rw source_fmor. rw source_ntrans. rw target_fmor. rw target_ntrans. rww H. am. am. nw. nw. am. am. nw. nw. nw. nw. nw. nw. nw. rww H. fw. nw. nw. nw. nw. fw. nw. nw. fw. nw. nw. nw. rw source_fmor. rw source_ntrans. rw target_ntrans. rw H0. rww H. am. fw. nw. nw. am. am. nw. nw. rw source_ntrans. rw target_fmor. rw target_ntrans. tv. am. am. nw. nw. am. fw. nw. nw. nw. fw. nw. nw. nw. fw. nw. nw. fw. nw. nw. rw mor_comp. tv. rw lem8. nw. rw H1. nw. nw. rww H. am. nw. rw source_ntrans. rw target_ntrans. wr H0. tv. am. fw. nw. nw. am. fw. nw. nw. rww source_ntrans. rw target_fmor. ap uneq. rw target_comp. rw target_ntrans. tv. am. am. nw. wr lem8. rw H1. nw. nw. rww H. nw. cw. nw. nw. nw. rww H. rw lem8. fw. nw. nw. nw. rw lemb. rw lem8. fw. nw. nw. fw. nw. nw. nw. cw. nw. fw. nw. nw. fw. nw. nw. nw. rw source_ntrans. rw target_fmor. rw target_ntrans. tv. am. am. nw. nw. am. fw. nw. nw. rw source_ntrans. rw target_fmor. rw target_ntrans. tv. am. am. nw. nw. am. fw. nw. nw. rw source_fmor. rw source_ntrans. rw target_comp. rw target_ntrans. wr H0. rww H. am. fw. nw. nw. nw. fw. nw. nw. fw. nw. nw. nw. rw source_ntrans. rw target_fmor. rw target_ntrans. tv. am. am. nw. nw. am. fw. nw. nw. am. am. nw. nw. am. rw target_vcompose. fw. nw. nw. uhg; ee. rww vcompose_axioms. sy; am. rww vcompose_axioms. sy; am. rw osource_vcompose. rww otarget_vcompose. rw osource_vcompose. am. rww osource_hcompose. Qed.
imports: Arith functor