diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index a5a2dd0f6..d77a0fd4d 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -54,10 +54,10 @@ has_zero.mk (of_nat 0)
 definition int_has_one [reducible] [instance] : has_one int :=
 has_one.mk (of_nat 1)
 
-theorem int_zero_eq_nat_zero : (0:int) = of_nat (0:nat) :=
+theorem of_nat_zero : of_nat (0:nat) = (0:int) :=
 rfl
 
-theorem int_one_eq_nat_one : (1:int) = of_nat (1:nat) :=
+theorem of_nat_one : of_nat (1:nat) = (1:int) :=
 rfl
 
 /- definitions of basic functions -/
diff --git a/library/data/int/div.lean b/library/data/int/div.lean
index b48961429..ce8aa4df4 100644
--- a/library/data/int/div.lean
+++ b/library/data/int/div.lean
@@ -108,8 +108,8 @@ by krewrite [divide.def, sign_zero, zero_mul]
 theorem div_one (a : ℤ) : a div 1 = a :=
 assert (1 : int) > 0, from dec_trivial,
 int.cases_on a
-  (take m : nat, by rewrite [int_one_eq_nat_one, -of_nat_div, nat.div_one])
-  (take m : nat, by rewrite [!neg_succ_of_nat_div this, int_one_eq_nat_one, -of_nat_div, nat.div_one])
+  (take m : nat, by rewrite [-of_nat_one, -of_nat_div, nat.div_one])
+  (take m : nat, by rewrite [!neg_succ_of_nat_div this, -of_nat_one, -of_nat_div, nat.div_one])
 
 theorem eq_div_mul_add_mod (a b : ℤ) : a = a div b * b + a mod b :=
 !add.comm ▸ eq_add_of_sub_eq rfl
diff --git a/library/data/int/gcd.lean b/library/data/int/gcd.lean
index 91dbbbfd7..6898ec424 100644
--- a/library/data/int/gcd.lean
+++ b/library/data/int/gcd.lean
@@ -265,7 +265,7 @@ theorem gcd_mul_left_cancel_of_coprime {c : ℤ} (a : ℤ) {b : ℤ} (H : coprim
    gcd (c * a) b = gcd a b :=
 begin
   revert H, unfold [coprime, gcd],
-  rewrite [int_one_eq_nat_one],
+  rewrite [-of_nat_one],
   rewrite [+of_nat_eq_of_nat_iff, nat_abs_mul],
   apply nat.gcd_mul_left_cancel_of_coprime,
 end
diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean
index 3d61536dc..552dacf99 100644
--- a/library/data/rat/basic.lean
+++ b/library/data/rat/basic.lean
@@ -364,10 +364,10 @@ has_zero.mk (0:int)
 definition rat_has_one [reducible] [instance] [priority rat.prio] : has_one rat :=
 has_one.mk (1:int)
 
-theorem rat_zero_eq_int_zero : (0:rat) = of_int (0:int) :=
+theorem of_int_zero : of_int (0:int) = (0:rat) :=
 rfl
 
-theorem rat_one_eq_int_one : (1:rat) = of_int (1:int) :=
+theorem of_int_one : of_int (1:int) = (1:rat) :=
 rfl
 
 protected definition add : ℚ → ℚ → ℚ :=
diff --git a/library/data/rat/order.lean b/library/data/rat/order.lean
index f75ebea24..b0016b47f 100644
--- a/library/data/rat/order.lean
+++ b/library/data/rat/order.lean
@@ -368,7 +368,7 @@ section
     begin
       rewrite [-mul_denom],
       apply mul_nonneg H,
-      rewrite [rat_zero_eq_int_zero, of_int_le_of_int_iff],
+      rewrite [-of_int_zero, of_int_le_of_int_iff],
       exact int.le_of_lt !denom_pos
     end,
   show num q ≥ 0, from le_of_of_int_le_of_int this
@@ -378,7 +378,7 @@ section
     begin
       rewrite [-mul_denom],
       apply mul_pos H,
-      rewrite [rat_zero_eq_int_zero, of_int_lt_of_int_iff],
+      rewrite [-of_int_zero, of_int_lt_of_int_iff],
       exact !denom_pos
     end,
   show num q > 0, from lt_of_of_int_lt_of_int this