proposition: Lemma ab_mul_homo {A B : AbGroup} (n : Int) (f : GroupHomomorphism A B) : grp_homo_compose f (ab_mul n) == grp_homo_compose (ab_mul n) f.
proof: Proof. intro x. induction n. - cbn. refine (grp_homo_inv _ _ @ _). refine (ap negate _). apply grp_pow_homo. - cbn. apply grp_homo_unit. - cbn. apply grp_pow_homo. Defined.
imports: Basics Spaces.Pos.Core Spaces.Int Algebra.AbGroups.AbelianGroup