{G : Group} (n : Int) : grp_pow (G:=G) mon_unit n = mon_unit. Proof. snrapply (int_iter_invariant n _ (fun g => g = mon_unit)); cbn. 1, 2: apply paths_ind_r. - apply grp_unit_r. - lhs nrapply grp_unit_r. apply grp_inv_unit. - reflexivity. Defined.
Require Import Basics Types HProp HFiber HSet. Require Import Homotopy.IdentitySystems. Require Import (notations) Classes.interfaces.canonical_names. Require Import Pointed.Core. Require Import WildCat. Require Import Spaces.Nat.Core Spaces.Int. Require Import Truncations.Core.