In #2050, a new definition of cyclic based on Int is introduced. Replacing the old one is a bit non-trivial however due to its extensive use.
It's also not clear if it is easy to show abgroup_Z is the free group on one generator. I had a quick look, but it seems awkward to prove.