Def pow_nat

feat(algebra/group_power): remove overloaded ^ notation, add smul

refactor(algebra/group,group_power): clean up proofs

refactor(*): import content from lean/library/data and library_dev