{G : Group} (n : Int) (g h : G) (c : g * h = h * g) : grp_pow (g * h) n = (grp_pow g n) * (grp_pow h n). Proof. induction n. - simpl. symmetry; nrapply grp_unit_r. - rewrite 3 grp_pow_succ. rewrite IHn. rewrite 2 grp_assoc. apply grp_cancelR. rewrite <- 2 grp_assoc. apply grp_cancelL. apply grp_pow_commutes. exact c^. - simpl. rewrite 3 grp_pow_pred. rewrite IHn. rewrite 2 grp_assoc. apply grp_cancelR. rewrite c. rewrite grp_inv_op. rewrite <- 2 grp_assoc. apply grp_cancelL. apply grp_pow_commutes. symmetry; apply grp_commutes_inv, c. 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.