{G : Group} (n : Int) (g h : G) (p : h * g = g * h) : h * (grp_pow g n) = (grp_pow g n) * h. Proof. induction n. - exact (grp_unit_r _ @ (grp_unit_l _)^). - rewrite grp_pow_succ. nrapply grp_commutes_op; assumption. - rewrite grp_pow_pred. nrapply grp_commutes_op. 2: assumption. apply grp_commutes_inv, p. 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.