grp_pow_commutes' {G : Group} (n : Int) (g : G) : g * grp_pow g n = grp_pow g n * g. Proof. by apply grp_pow_commutes. 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.