{A B : AbGroup} (f : GroupHomomorphism A B) (n : Int) : f o ab_mul n == ab_mul n o f := grp_pow_natural f n.
Require Import Basics Types. Require Import Spaces.Nat.Core Spaces.Int. Require Import Algebra.Groups.QuotientGroup. Require Import WildCat.