diff --git a/hott/algebra/inf_group.hlean b/hott/algebra/inf_group.hlean
index 5a8009b43..6823d23b6 100644
--- a/hott/algebra/inf_group.hlean
+++ b/hott/algebra/inf_group.hlean
@@ -141,17 +141,6 @@ definition add_comm_inf_semigroup_of_add_comm_inf_monoid [reducible] [trans_inst
   [H : add_comm_inf_monoid A] : add_comm_inf_semigroup A :=
 @comm_inf_monoid.to_comm_inf_semigroup A H
 
-section add_comm_inf_monoid
-  variables [s : add_comm_inf_monoid A]
-  include s
-
-  theorem add_comm_three  (a b c : A) : a + b + c = c + b + a :=
-    by rewrite [{a + _}add.comm, {_ + c}add.comm, -*add.assoc]
-
-  theorem add.comm4 : Π (n m k l : A), n + m + (k + l) = n + k + (m + l) :=
-  comm4 add.comm add.assoc
-end add_comm_inf_monoid
-
 /- group -/
 
 structure inf_group [class] (A : Type) extends inf_monoid A, has_inv A :=
@@ -609,8 +598,16 @@ namespace norm_num
 
 definition add1 [s : has_add A] [s' : has_one A] (a : A) : A := add a one
 
-theorem add_comm_four [s : add_comm_inf_semigroup A] (a b : A) : a + a + (b + b) = (a + b) + (a + b) :=
-  by rewrite [-add.assoc at {1}, add.comm, {a + b}add.comm at {1}, *add.assoc]
+theorem add_comm_three [s : add_comm_inf_semigroup A] (a b c : A) : a + b + c = c + b + a :=
+  by rewrite [{a + _}add.comm, {_ + c}add.comm, -*add.assoc]
+
+theorem add.comm4 [s : add_comm_inf_semigroup A] :
+  Π (n m k l : A), n + m + (k + l) = n + k + (m + l) :=
+comm4 add.comm add.assoc
+
+theorem add_comm_four [s : add_comm_inf_semigroup A] (a b : A) :
+  a + a + (b + b) = (a + b) + (a + b) :=
+!add.comm4
 
 theorem add_comm_middle [s : add_comm_inf_semigroup A] (a b c : A) : a + b + c = a + c + b :=
   by rewrite [add.assoc, add.comm b, -add.assoc]
diff --git a/hott/init/pointed.hlean b/hott/init/pointed.hlean
index bde775b40..caa01ab1c 100644
--- a/hott/init/pointed.hlean
+++ b/hott/init/pointed.hlean
@@ -112,7 +112,7 @@ namespace pointed
 
   abbreviation respect_pt [unfold 3] := @pmap.resp_pt
   notation `map₊` := pmap
-  infix ` →* `:30 := pmap
+  infix ` →* `:28 := pmap
   attribute pmap.to_fun ppi_gen.to_fun [coercion]
   -- notation `Π*` binders `, ` r:(scoped P, ppi _ P) := r
   -- definition pmap.mk [constructor] {A B : Type*} (f : A → B) (p : f pt = pt) : A →* B :=
diff --git a/hott/types/nat/hott.hlean b/hott/types/nat/hott.hlean
index 874883dbc..4cc9ac044 100644
--- a/hott/types/nat/hott.hlean
+++ b/hott/types/nat/hott.hlean
@@ -161,10 +161,13 @@ namespace nat
 
   attribute is_succ.mk [instance]
 
+  definition is_succ_1 [instance] : is_succ 1 := is_succ.mk 0
+
   definition is_succ_add_right [instance] [constructor] (n m : ℕ) [H : is_succ m] : is_succ (n+m) :=
   by induction H with m; constructor
 
-  definition is_succ_add_left [instance] [constructor] (n m : ℕ) [H : is_succ n] : is_succ (n+m) :=
+  definition is_succ_add_left [instance] [priority 900] [constructor] (n m : ℕ) [H : is_succ n] :
+    is_succ (n+m) :=
   by induction H with n; cases m with m: constructor
 
   definition is_succ_bit0 [constructor] (n : ℕ) [H : is_succ n] : is_succ (bit0 n) :=
diff --git a/hott/types/pointed2.hlean b/hott/types/pointed2.hlean
index c38b65ad7..faaf5c4aa 100644
--- a/hott/types/pointed2.hlean
+++ b/hott/types/pointed2.hlean
@@ -554,7 +554,7 @@ namespace pointed
   phomotopy.mk (λa, respect_pt f) (idp_con _)⁻¹
 
   definition pconst_pcompose [constructor] (f : A →* B) : pconst B C ∘* f ~* pconst A C :=
-  phomotopy.mk (λa, rfl) (ap_constant _ _)⁻¹
+  phomotopy.mk (λa, rfl) !ap_constant⁻¹
 
   definition ppcompose_left [constructor] (g : B →* C) : ppmap A B →* ppmap A C :=
   pmap.mk (pcompose g) (eq_of_phomotopy (pcompose_pconst g))
@@ -562,7 +562,7 @@ namespace pointed
   definition ppcompose_right [constructor] (f : A →* B) : ppmap B C →* ppmap A C :=
   pmap.mk (λg, g ∘* f) (eq_of_phomotopy (pconst_pcompose f))
 
-  /- TODO: give construction using pequiv.MK, which computes better (see comment for a start of the proof) -/
+  /- TODO: give construction using pequiv.MK, which computes better (see comment for a start of the proof), rename to ppmap_pequiv_ppmap_right -/
   definition pequiv_ppcompose_left [constructor] (g : B ≃* C) : ppmap A B ≃* ppmap A C :=
   pequiv.MK' (ppcompose_left g) (ppcompose_left g⁻¹ᵉ*)
     begin intro f, apply eq_of_phomotopy, apply pinv_pcompose_cancel_left end
diff --git a/library/data/int/order.lean b/library/data/int/order.lean
index 81052110d..1ba1910da 100644
--- a/library/data/int/order.lean
+++ b/library/data/int/order.lean
@@ -313,10 +313,10 @@ theorem le_of_lt_add_one {a b : ℤ} (H : a < b + 1) : a ≤ b :=
 have H1 : a + 1 ≤ b + 1, from add_one_le_of_lt H,
 le_of_add_le_add_right H1
 
-theorem sub_one_le_of_lt {a b : ℤ} (H : a ≤ b) : a - 1 < b :=
+theorem sub_one_lt_of_le {a b : ℤ} (H : a ≤ b) : a - 1 < b :=
 lt_of_add_one_le (begin rewrite sub_add_cancel, exact H end)
 
-theorem lt_of_sub_one_le {a b : ℤ} (H : a - 1 < b) : a ≤ b :=
+theorem le_of_sub_one_lt {a b : ℤ} (H : a - 1 < b) : a ≤ b :=
 !sub_add_cancel ▸ add_one_le_of_lt H
 
 theorem le_sub_one_of_lt {a b : ℤ} (H : a < b) : a ≤ b - 1 :=