{A : AbGroup} : GroupIsomorphism A A. Proof. snrapply Build_GroupIsomorphism. - snrapply Build_GroupHomomorphism. + exact (fun a => -a). + intros x y. refine (grp_inv_op x y @ _). apply commutativity. - srapply isequiv_adjointify. 1: exact (fun a => -a). 1-2: exact negate_involutive. Defined.
Require Import Basics Types. Require Import Spaces.Nat.Core Spaces.Int. Require Import Algebra.Groups.QuotientGroup. Require Import WildCat.