proposition: Lemma oppnt'_oppnt' : forall u, Nat_Trans.axioms u -> oppnt' (oppnt' u) = u.
proof: Proof. ir. ap axioms_extensionality. ap oppnt'_axioms. ap oppnt'_axioms. am. am. rw source_oppnt'. rw target_oppnt'. rw oppf_oppf. tv. uh H; ee. rw target_oppnt'. rw source_oppnt'. rw oppf_oppf. tv. ir. rw ntrans_oppnt'. rw ntrans_oppnt'. rw flip_flip. tv. am. rwi osource_oppnt' H0. rwi ob_opp H0. rwi osource_oppnt' H0. rwi ob_opp H0. am. am. app oppnt'_axioms. app oppnt'_axioms. rwi osource_oppnt' H0. rwi ob_opp H0. am. app oppnt'_axioms. Qed.
imports: Arith functor