{G: Group} (m : Int) (g : G) : grp_pow g (- m)%int = - grp_pow g m. Proof. apply grp_moveL_1V. lhs_V nrapply grp_pow_add. by rewrite int_add_neg_l. 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.