proposition: Lemma oppnt'_axioms : forall u, Nat_Trans.axioms u -> Nat_Trans.axioms (oppnt' u).
proof: Proof. ir. cp H. uh H0; ee. uhg; ee. uf oppnt'. ap create_like. rw osource_oppnt'. ap opp_axioms. am. am. rw otarget_oppnt'. ap opp_axioms. am. am. rw source_oppnt'. ap oppf_axioms. am. rw target_oppnt'. ap oppf_axioms. am. rw target_oppnt'. rw source_oppf. rw osource_oppnt'. tv. am. am. rw source_oppnt'. rw target_oppf. rw otarget_oppnt'. tv. am. ir. am. rw otarget_oppnt'. ir. rwi osource_oppnt' H11. rwi ob_opp H11. rw ntrans_oppnt'. rw mor_opp. rw flip_flip. app mor_ntrans. am. am. am. am. ir. rwi osource_oppnt' H11. rwi ob_opp H11. rw ntrans_oppnt'. rw source_flip. rw source_oppnt'. rw fob_oppf. rw target_ntrans. tv. am. am. am. rw source_oppf. rw source_target. rw ob_opp. am. am. am. assert (mor (otarget u) (ntrans u x)). ap mor_ntrans. am. am. tv. apply mor_arrow_like with (otarget u). am. am. am. am. ir. cp H11. rwi osource_oppnt' H12. rwi ob_opp H12. rw ntrans_oppnt'. rw target_flip. rw target_oppnt'. rw fob_oppf. rw source_ntrans. tv. am. am. am. rw source_oppf. rw ob_opp. am. rww functor_axioms_source. apply mor_arrow_like with (otarget u). ap mor_ntrans. am. am. tv. am. am. am. ir. cp H11. rwi osource_oppnt' H12. cp H12. rwi mor_opp H13. rw otarget_oppnt'. rw target_oppnt'. rw ntrans_oppnt'. rw ntrans_oppnt'. rw fmor_oppf. rw source_oppnt'. rw fmor_oppf. rw comp_opp. rw flip_flip. rw comp_opp. rw flip_flip. rw flip_flip. rw flip_flip. assert (source u0 = target (flip u0)). rww target_flip. apply mor_arrow_like with (osource (oppnt' u)). am. rw H14. ap uneq. rw H10. rw source_flip. tv. apply mor_arrow_like with (osource (oppnt' u)). am. am. rw mor_opp. rw flip_flip. wr target_source. ap mor_fmor. am. am. am. rw mor_opp. rw flip_flip. ap mor_ntrans. am. wr target_flip. rww ob_target. apply mor_arrow_like with (osource (oppnt' u)). am. tv. rw source_flip. rw target_flip. rw source_ntrans. rw target_fmor. ap uneq. rw target_flip. tv. apply mor_arrow_like with (opp (osource u)); am. am. am. am. wr target_flip. rww ob_target. apply mor_arrow_like with (opp (osource u)); am. apply mor_arrow_like with (otarget u). ap mor_ntrans. am. wr target_flip. rww ob_target. apply mor_arrow_like with (opp (osource u)); am. tv. apply mor_arrow_like with (target (source u)). ap mor_fmor. am. am. rw mor_opp. rw flip_flip. ap mor_ntrans. am. wr source_flip. rww ob_source. apply mor_arrow_like with (osource (oppnt' u)). am. tv. rw mor_opp. rw flip_flip. uf otarget. ap mor_fmor. am. rww source_target. rw source_flip. rw target_flip. rw target_ntrans. rw source_fmor. ap uneq. rw source_flip. tv. apply mor_arrow_like with (osource (oppnt' u)). am. am. rw source_target. am. am. am. wr source_flip. rww ob_source. apply mor_arrow_like with (osource (oppnt' u)). am. apply mor_arrow_like with (target (target u)). app mor_fmor. rw source_target. am. am. apply mor_arrow_like with (otarget u). app mor_ntrans. wr source_flip. rww ob_source. apply mor_arrow_like with (osource (oppnt' u)). am. rww functor_axioms_target. rw source_oppf. rww source_target. rww functor_axioms_target. rww functor_axioms_source. rw source_oppf. am. am. am. wr target_flip. rww ob_target. apply mor_arrow_like with (osource (oppnt' u)). am. am. wr source_flip. rww ob_source. apply mor_arrow_like with (osource (oppnt' u)). am. am. am. Qed.
imports: Arith functor