Theorem nat.gcd_eq_one_of_coprime

feat(data/nat): better sqrt + pairing, prime numbers, renames...

refactor(*): use 'lemma' iff statement is private

refactor(*): import content from lean/library/data and library_dev