(z z' : Int) : ab_mul (A:=abgroup_Z) z z' = z * z'. Proof. induction z. - reflexivity. - cbn. lhs nrapply (grp_pow_succ (G:=abgroup_Z)). rhs nrapply int_mul_succ_l. f_ap. - cbn. lhs nrapply (grp_pow_pred (G:=abgroup_Z)). rhs nrapply int_mul_pred_l. f_ap. Defined.
Require Import Basics. Require Import Spaces.Pos.Core Spaces.Int. Require Import Algebra.AbGroups.AbelianGroup.