feat(data/nat/gcd): add simple lemmas (#1382)
feat(data/nat/gcd): add simple lemmas (#1382)

* feat(data/nat/gcd): more simple lemmas

* Prove `iff` instead of one side implication

leanprover-community/mathlib,leanprover-community/mathlib