proposition: Lemma are_finverse_opp_fc_fc_opp : forall a b, Category.axioms a -> Category.axioms b -> are_finverse (opp_fc a b) (fc_opp a b).
proof: Proof. ir. assert (Functor.axioms (opp_fc a b)). app opp_fc_axioms. assert (Functor.axioms (fc_opp a b)). app fc_opp_axioms. assert (source (fc_opp a b) = target (opp_fc a b)). rw source_fc_opp. rww target_opp_fc. assert (source (opp_fc a b) = target (fc_opp a b)). rw target_fc_opp. rww source_opp_fc. uhg; ee. am. am. am. am. ap Functor.axioms_extensionality. ap fcompose_axioms. am. am. am. rw fidentity_axioms. tv. rw source_fc_opp. ap functor_cat_axioms. app opp_axioms. app opp_axioms. rw source_fcompose. rw source_fidentity. reflexivity. rw target_fcompose. rw target_fidentity. sy; am. ir. rwi source_fcompose H5. cp H5. rwi source_fc_opp H6. cp H6. rwi mor_functor_cat H7. uh H7; ee. rw fmor_fcompose. rw fmor_fidentity. rw fmor_opp_fc. rw fmor_fc_opp. rw flip_flip. rw oppnt_oppnt. tv. am. wr target_fc_opp. ap mor_fmor. ap fc_opp_axioms. am. am. am. am. app opp_fc_axioms. app fc_opp_axioms. am. am. app opp_axioms. app opp_axioms. ap Functor.axioms_extensionality. ap fcompose_axioms. am. am. am. rw fidentity_axioms. tv. rw source_opp_fc. ap opp_axioms. app functor_cat_axioms. rw source_fcompose. rw source_fidentity. reflexivity. rw target_fcompose. rw target_fidentity. sy; am. ir. rwi source_fcompose H5. cp H5. rwi source_opp_fc H6. cp H6. rwi mor_opp H7. cp H7. rwi mor_functor_cat H8. uh H8; ee. rw fmor_fcompose. rw fmor_fidentity. rw fmor_fc_opp. rw fmor_opp_fc. rw oppnt_oppnt. rw flip_flip. tv. am. wr target_opp_fc. ap mor_fmor. ap opp_fc_axioms. am. am. am. am. app fc_opp_axioms. app opp_fc_axioms. am. am. am. am. Qed.
imports: Arith nat_trans