{G : Group} (m n : Int) (g : G) : grp_pow g (n + m)%int = grp_pow g n * grp_pow g m. Proof. lhs nrapply int_iter_add. induction n; cbn. 1: exact (grp_unit_l _)^. 1: rewrite int_iter_succ_l, grp_pow_succ. 2: rewrite int_iter_pred_l, grp_pow_pred; cbn. 1,2 : rhs_V srapply associativity; apply ap, 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.