Data/Nat/Gcd.lean

Stream: mathlib4

[David Renshaw]

I ported most of data/nat/gcd.lean to mathlib4:
https://github.com/leanprover-community/mathlib4/pull/20

[David Renshaw]

I needed a bunch of divisibility results from the as-yet-unported algebra/divisibility.lean. For this exercise, I just proved specialized Nat versions of those results.