{G : Group} (m n : Int) (g : G) : grp_pow g (m * n)%int = grp_pow (grp_pow g m) n. Proof. induction n. - simpl. by rewrite int_mul_0_r. - rewrite int_mul_succ_r. rewrite grp_pow_add. rewrite grp_pow_succ. apply grp_cancelL, IHn. - rewrite int_mul_pred_r. rewrite grp_pow_add. rewrite grp_pow_neg_inv. rewrite grp_pow_pred. apply grp_cancelL, IHn. 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.