add Nat_iter_mul

Ralf Jungrequested to merge
ralf/nat-iter-mul into master

Original proof by Joshua Yanovski

Edited by Ralf Jung

Merge request reports