feat(data/nat/gcd.lean): port from Lean 3 (except for pow_dvd_pow_iff) (

#20)

* port data/nat/gcd.lean (except for pow_dvd_pow_iff)

* minor touchup

* move Dvd class and notation to top level file, like Mem

* add copyright header

* add missing imports

* gcd_induction -> gcd.induction

* simplify usages of gcd.induction via the 'induction' tactic

* remove unused import

* tiny simplification of gcd_rec proof

* use eq_zero_of_mul_eq_zero

Mathlib.lean

@@ -10,7 +10,9 @@ import Mathlib.Data.Equiv.Basic
 import Mathlib.Data.Equiv.Functor
 import Mathlib.Data.List.Basic
 import Mathlib.Data.Nat.Basic
+import Mathlib.Data.Nat.Gcd
 import Mathlib.Data.UInt
+import Mathlib.Dvd
 import Mathlib.Function
 import Mathlib.Logic.Basic
 import Mathlib.Logic.Function.Basic

Mathlib/Data/Nat/Basic.lean

@@ -157,6 +157,10 @@ lemma eq_of_mul_eq_mul_left {m k n : ℕ} (Hn : 0 < n) (H : n * m = n * k) : m =
 Nat.le_antisymm (Nat.le_of_mul_le_mul_left (Nat.le_of_eq H) Hn)
                 (Nat.le_of_mul_le_mul_left (Nat.le_of_eq H.symm) Hn)
 
+lemma eq_of_mul_eq_mul_right {n m k : ℕ} (Hm : 0 < m) (H : n * m = k * m) : n = k :=
+by rw [Nat.mul_comm n m, Nat.mul_comm k m] at H
+   exact Nat.eq_of_mul_eq_mul_left Hm H
+
 protected lemma add_self_ne_one : ∀ (n : ℕ), n + n ≠ 1
 | n+1, h =>
   have h1 : succ (succ (n + n)) = 1 := succ_add n n ▸ h