Commit 2020-05-27 21:30 efb4e959

refactor(iterate): move to function; renamings (#2832)

• move lemmas about iterate from data.nat.basic to logic.function.iterate;
• move lemmas like nat.iterate_succ to function namespace;
• rename some lemmas:
  • iterate₀ to iterate_fixed,
  • iterate₁ to semiconj.iterate_right, see also commute.iterate_left and commute.iterate_right;
  • iterate₂ to semiconj₂.iterate;
  • iterate_cancel to left_inverse.iterate and right_inverse.iterate;
• move lemmas *_hom.iterate_map_* to algebra/iterate_hom.