proposition: Lemma Z1_mul_nat_beta {A : AbGroup} (a : A) (n : nat) : Z1_rec a (nat_to_Z1 n) = ab_mul_nat n a.
proof: Proof. induction n as [|n H]. 1: easy. refine (grp_pow_homo _ _ _ @ _); simpl. by rewrite grp_unit_r. Defined.
imports: Basics Types WildCat.Core Truncations.Core AbelianGroup AbHom Centralizer AbProjective Groups.FreeGroup AbGroups.Z Int.Core