diff --git a/Cubical/Data/Int/GCD.agda b/Cubical/Data/Int/GCD.agda
new file mode 100644
index 0000000000..b1053bf3fe
--- /dev/null
+++ b/Cubical/Data/Int/GCD.agda
@@ -0,0 +1,60 @@
+module Cubical.Data.Int.GCD where
+
+open import Cubical.Data.Empty as ⊥
+import Cubical.Data.Nat.GCD as ℕ
+open import Cubical.Data.Nat.Divisibility renaming (_∣_ to _∣ℕ_)
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Int.Divisibility
+open import Cubical.Data.Int
+
+------------------------------------------------------------------------
+-- Definition
+------------------------------------------------------------------------
+
+gcd : ℤ → ℤ → ℤ
+gcd i j = pos (ℕ.gcd  (abs i) (abs j))
+
+gcd-def : ∀ i j → gcd i j ≡ pos (ℕ.gcd (abs i) (abs j))
+gcd-def i j = refl
+
+gcdSym : ∀ i j → gcd i j ≡ gcd j i
+gcdSym i j = cong pos (ℕ.gcdSym (abs i) (abs j))
+
+------------------------------------------------------------------------
+-- ℕ and ℤ conversions
+------------------------------------------------------------------------
+
+gcd∣ℕ→∣ℤ-lemma : ∀ {i j k : ℤ} → ℕ.gcd (abs i) (abs j) ∣ℕ (abs k) → gcd i j ∣ k
+gcd∣ℕ→∣ℤ-lemma {i}{j}{k} gcdij|k = ∣ℕ→∣ gcdij|k
+
+ℕ∣gcd→ℤ∣-lemma : ∀ {i j k : ℤ} →  (abs k) ∣ℕ ℕ.gcd (abs i) (abs j) → k ∣ gcd i j
+ℕ∣gcd→ℤ∣-lemma {i}{j}{k} k|gcdij = ∣ℕ→∣ k|gcdij
+
+gcd∣ℤ→∣ℕ-lemma : ∀ {i j k : ℤ} → gcd i j ∣ k → ℕ.gcd (abs i) (abs j) ∣ℕ (abs k)
+gcd∣ℤ→∣ℕ-lemma {i}{j}{k} gcdij|k = ∣→∣ℕ gcdij|k
+
+ℤ∣gcd→ℕ∣-lemma : ∀ {i j k : ℤ} → k ∣ gcd i j → (abs k) ∣ℕ ℕ.gcd (abs i) (abs j)
+ℤ∣gcd→ℕ∣-lemma {i}{j}{k} k|gcdij = ∣→∣ℕ k|gcdij
+
+------------------------------------------------------------------------
+-- Properties
+------------------------------------------------------------------------
+
+gcd[i,j]∣i : ∀ i j → gcd i j ∣ i
+gcd[i,j]∣i i j = gcd∣ℕ→∣ℤ-lemma {i}{j} (ℕ.gcd[m,n]∣m (abs i) (abs j))
+
+gcd[i,j]∣j : ∀ i j → gcd i j ∣ j
+gcd[i,j]∣j i j = gcd∣ℕ→∣ℤ-lemma {i}{j} (ℕ.gcd[m,n]∣n (abs i) (abs j))
+
+gcd-greatest : ∀ {i j c} → c ∣ i → c ∣ j → c ∣ gcd i j
+gcd-greatest {i}{j}{c} ci cj =
+  ℕ∣gcd→ℤ∣-lemma {i}{j}{c} (ℕ.gcd-greatest (∣→∣ℕ ci) (∣→∣ℕ cj))
+
+gcd[0,0]≡0 : gcd 0 0 ≡ 0
+gcd[0,0]≡0  = cong pos ℕ.gcd[0,0]≡0
+
+gcd[i,j]≡0⇒i≡0 : ∀ {i j} → gcd i j ≡ 0 → i ≡ 0
+gcd[i,j]≡0⇒i≡0 {i} {j} eqn = abs≡0 i (ℕ.gcd[m,n]≡0⇒m≡0 {abs i}{abs j} (injPos eqn))
+
+gcd[i,j]≡0⇒j≡0 : ∀ {i j} → gcd i j ≡ 0 → j ≡ 0
+gcd[i,j]≡0⇒j≡0 {i}{j} eqn = gcd[i,j]≡0⇒i≡0 {j}{i} (gcdSym j i ∙ eqn)
diff --git a/Cubical/Data/Nat/Base.agda b/Cubical/Data/Nat/Base.agda
index 545dbadb90..82ef9f7cb5 100644
--- a/Cubical/Data/Nat/Base.agda
+++ b/Cubical/Data/Nat/Base.agda
@@ -71,6 +71,10 @@ isZero : ℕ → Bool
 isZero zero = true
 isZero (suc n) = false
 
+NonZero : ℕ → Type
+NonZero zero = ⊥
+NonZero (ℕ.suc n) = Unit
+
 -- exponential
 
 _^_ : ℕ → ℕ → ℕ
diff --git a/Cubical/Data/Nat/Coprime.agda b/Cubical/Data/Nat/Coprime.agda
index a7833ef250..6e7139e49f 100644
--- a/Cubical/Data/Nat/Coprime.agda
+++ b/Cubical/Data/Nat/Coprime.agda
@@ -16,6 +16,12 @@ open import Cubical.Data.Nat.GCD
 areCoprime : ℕ × ℕ → Type₀
 areCoprime (m , n) = isGCD m n 1
 
+zeroCoprime : {d-1 : ℕ} → (copr : areCoprime (0 , ℕ.suc d-1)) → d-1 ≡ 0
+zeroCoprime {d-1} copr = injSuc (zeroGCD-unique (symGCD copr))
+
+isPropAreCoprime : (x : ℕ) (y : ℕ) → isProp (areCoprime (x , y))
+isPropAreCoprime x y = isPropIsGCD
+
 -- Any pair (m , n) can be converted to a coprime pair (m' , n') s.t.
 --  m' ∣ m, n' ∣ n if and only if one of m or n is nonzero
 
diff --git a/Cubical/Data/Nat/GCD.agda b/Cubical/Data/Nat/GCD.agda
index d425978e55..f7df22ea06 100644
--- a/Cubical/Data/Nat/GCD.agda
+++ b/Cubical/Data/Nat/GCD.agda
@@ -3,17 +3,17 @@ module Cubical.Data.Nat.GCD where
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.HLevels
-open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Isomorphism
 
 open import Cubical.Induction.WellFounded
 
 open import Cubical.Data.Sigma as Σ
-open import Cubical.Data.Fin   as F hiding (_%_ ; _/_)
-open import Cubical.Data.NatPlusOne
+open import Cubical.Data.Sum
+open import Cubical.Data.Fin as F hiding (_%_ ; _/_)
 
 open import Cubical.HITs.PropositionalTruncation as PropTrunc
 
+open import Cubical.Data.Empty as ⊥
 open import Cubical.Data.Nat.Base
 open import Cubical.Data.Nat.Properties
 open import Cubical.Data.Nat.Order
@@ -27,7 +27,7 @@ open import Cubical.Relation.Nullary
 
 private
   variable
-    m n d : ℕ
+    m n c d : ℕ
 
 -- common divisors
 
@@ -55,7 +55,6 @@ isPropGCD : isProp (GCD m n)
 isPropGCD (d , dCD , gr) (d' , d'CD , gr') =
   Σ≡Prop (λ _ → isPropIsGCD) (antisym∣ (gr' d dCD) (gr d' d'CD))
 
-
 symGCD : isGCD m n d → isGCD n m d
 symGCD (dCD , gr) = symCD dCD , λ { d' d'CD → gr d' (symCD d'CD) }
 
@@ -65,11 +64,21 @@ divsGCD p = (∣-refl refl , p) , λ { d (d∣m , _) → d∣m }
 oneGCD : ∀ m → isGCD m 1 1
 oneGCD m = symGCD (divsGCD (∣-oneˡ m))
 
-
 -- The base case of the Euclidean algorithm
 zeroGCD : ∀ m → isGCD m 0 m
 zeroGCD m = divsGCD (∣-zeroʳ m)
 
+-- zeroGCD-unique lemma: if d is gcd of m and 0, then d ≡ m
+zeroGCD-unique : {m d : ℕ} → isGCD m 0 d → m ≡ d
+zeroGCD-unique {m} {d} (iscd , greatest) =
+  let
+    d∣m = fst iscd
+    m∣m = ∣-refl (refl {x = m})
+    m∣0 = ∣-zeroʳ m
+    m∣d = greatest m (m∣m , m∣0)
+  in
+  antisym∣ m∣d d∣m
+
 -- a pair of useful lemmas about ∣ and (efficient) %
 private
   ∣→∣% : ∀ {m n d} → d ∣ m → d ∣ n → d ∣ (m % n)
@@ -159,7 +168,6 @@ euclid m n@(suc n-1) =
   in
     r .fst , stepGCD (r .snd)
 
-
 isContrGCD : ∀ m n → isContr (GCD m n)
 isContrGCD m n = euclid m n , isPropGCD _
 
@@ -177,6 +185,16 @@ isGCD→gcd≡ dGCD = cong fst (isContrGCD _ _ .snd (_ , dGCD))
 gcd≡→isGCD : gcd m n ≡ d → isGCD m n d
 gcd≡→isGCD p = subst (isGCD _ _) p (gcdIsGCD _ _)
 
+gcd≡isGCD : ∀ m n d → (gcd m n ≡ d) ≡ (isGCD m n d)
+gcd≡isGCD m n d = isoToPath (iso gcd≡→isGCD isGCD→gcd≡
+  (λ b → isPropIsGCD (gcd≡→isGCD (isGCD→gcd≡ b)) b)
+  (λ a →  isSetℕ (gcd m n) d (isGCD→gcd≡ {m}{n}{d} (gcd≡→isGCD a)) a))
+
+uniqueGCD : ∀ {d'} → isGCD m n d → isGCD m n d' → d ≡ d'
+uniqueGCD isgd isgd' = sym (isGCD→gcd≡ isgd) ∙ isGCD→gcd≡ isgd'
+
+gcdSym : (m n : ℕ) → (gcd m n) ≡ (gcd n m)
+gcdSym m n =  uniqueGCD (gcdIsGCD m n) (symGCD (gcdIsGCD n m))
 
 -- multiplicative properties of the gcd
 
@@ -214,6 +232,36 @@ isGCD-multʳ {m} {n} {d} k dGCD = gcd≡→isGCD (gcd-factorʳ m n k ∙ cong (_
   where r : gcd m n ≡ d
         r = isGCD→gcd≡ dGCD
 
+-- Core properties of gcd
+
+gcd[m,n]∣m : (m n : ℕ) → (gcd m n) ∣ m
+gcd[m,n]∣m m n = fst (fst (gcdIsGCD m n))
+
+gcd[m,n]∣n : (m n : ℕ) → (gcd m n) ∣ n
+gcd[m,n]∣n m n = transport (cong (λ a → a ∣ n) (gcdSym n m) ) (gcd[m,n]∣m n m)
+
+gcd-greatest : c ∣ m → c ∣ n → c ∣ gcd m n
+gcd-greatest = curry (snd (gcdIsGCD _ _) _)
+
+-- Other properties
+
+gcd[0,0]≡0 : gcd 0 0 ≡ 0
+gcd[0,0]≡0 = antisym∣ (∣-zeroʳ (gcd 0 0) ) (gcd-greatest (∣-zeroʳ 0) (∣-zeroʳ 0))
+
+gcd[m,n]≢0 : ∀ (m n : ℕ) → (¬ (m ≡ 0)) ⊎ (¬ (n ≡ 0)) → ¬ (gcd m n ≡ 0)
+gcd[m,n]≢0 m n (inl m≢0) gcd0 =
+  m≢0 (sym (∣-zeroˡ (transport (cong (λ a → a ∣ m) gcd0) (gcd[m,n]∣m m n))))
+gcd[m,n]≢0 m n (inr n≢0) gcd0 =
+  n≢0 (sym (∣-zeroˡ (transport ((cong (λ a → a ∣ n) gcd0)) (gcd[m,n]∣n m n))))
+
+gcd[m,n]≡0⇒m≡0 : gcd m n ≡ 0 → m ≡ 0
+gcd[m,n]≡0⇒m≡0 {zero} {n} gmn = refl
+gcd[m,n]≡0⇒m≡0 {suc m} {n} gmn =
+  ⊥.elim {A = λ bot → suc m ≡ 0} (gcd[m,n]≢0 (suc m) n (inl snotz) gmn)
+
+gcd[m,n]≡0⇒n≡0 : ∀ {m n} → gcd m n ≡ 0 → n ≡ 0
+gcd[m,n]≡0⇒n≡0 {m}{n} gmn = gcd[m,n]≡0⇒m≡0 {n} {m} (gcdSym n m ∙ gmn)
+
 -- Inequality for strict divisibility
 
 stDivIneqGCD : ¬ m ≡ 0 → ¬ m ∣ n → (g : GCD m n) → g .fst < m