proposition: Lemma Z_to_group_nat_eq_pos : forall (n : Z) (g : G), Equal (Z_to_group_nat_fun g n) (Z_to_group_fun g n).
proof: Proof. intros n g; try assumption. apply Trans with (Ap (sgroup_map (monoid_sgroup_hom (Z_to_group_nat g))) n); auto with algebra. apply Sym. apply Z_to_group_fun_eq. Qed.
imports: Z_group