diff --git a/library/data/int/gcd.lean b/library/data/int/gcd.lean
index 24fbf9dfb8..dddb7e0ab4 100644
--- a/library/data/int/gcd.lean
+++ b/library/data/int/gcd.lean
@@ -42,19 +42,18 @@ by rewrite [↑gcd, *nat_abs_abs]
 theorem gcd_abs_abs (a b : ℤ) : gcd (abs a) (abs b) = gcd a b :=
 by rewrite [↑gcd, *nat_abs_abs]
 
+section
+open nat
 theorem gcd_of_ne_zero (a : ℤ) {b : ℤ} (H : b ≠ 0) : gcd a b = gcd b (abs a mod abs b) :=
-sorry
-/-
-have nat_abs b ≠ nat.zero,        from assume H', H (eq_zero_of_nat_abs_eq_zero H'),
-have (#nat nat_abs b > nat.zero), from nat.pos_of_ne_zero this,
-assert nat.gcd (nat_abs a) (nat_abs b) = (#nat nat.gcd (nat_abs b) (nat_abs a mod nat_abs b)),
+have nat_abs b ≠ 0,  from assume H', H (eq_zero_of_nat_abs_eq_zero H'),
+have nat_abs b > 0,  from pos_of_ne_zero this,
+assert nat.gcd (nat_abs a) (nat_abs b) = (nat.gcd (nat_abs b) (nat_abs a mod nat_abs b)),
   from @nat.gcd_of_pos (nat_abs a) (nat_abs b) this,
 calc
- gcd a b = nat.gcd (nat_abs b) (#nat nat_abs a mod nat_abs b) : by rewrite [↑gcd, this]
-     ... = gcd (abs b) (abs a mod abs b)                      :
-               by rewrite [↑gcd, -*of_nat_nat_abs, of_nat_mod]
-     ... = gcd b (abs a mod abs b)                            : by rewrite [↑gcd, *nat_abs_abs]
--/
+ gcd a b = nat.gcd (nat_abs b) (nat_abs a mod nat_abs b) : by rewrite [↑gcd, this]
+     ... = gcd (abs b) (abs a mod abs b)                 : by rewrite [↑gcd, -*of_nat_nat_abs, of_nat_mod]
+     ... = gcd b (abs a mod abs b)                       : by rewrite [↑gcd, *nat_abs_abs]
+end
 
 theorem gcd_of_pos (a : ℤ) {b : ℤ} (H : b > 0) : gcd a b = gcd b (abs a mod b) :=
 by rewrite [!gcd_of_ne_zero (ne_of_gt H), abs_of_pos H]