diff --git a/archive/imo/imo2008_q4.lean b/archive/imo/imo2008_q4.lean
index 74230a759b263..28aebcc150af4 100644
--- a/archive/imo/imo2008_q4.lean
+++ b/archive/imo/imo2008_q4.lean
@@ -23,13 +23,8 @@ The desired theorem is that either `f = λ x, x` or `f = λ x, 1/x`
 open real
 
 lemma abs_eq_one_of_pow_eq_one (x : ℝ) (n : ℕ) (hn : n ≠ 0) (h : x ^ n = 1) : abs x = 1 :=
-begin
-  let x₀ := real.to_nnreal (abs x),
-  have h' : (abs x) ^ n = 1, { rwa [pow_abs, h, abs_one] },
-  have : (x₀ : ℝ) ^ n = 1, rw (real.coe_to_nnreal (abs x) (abs_nonneg x)), exact h',
-  have : x₀ = 1 := eq_one_of_pow_eq_one hn (show x₀ ^ n = 1, by assumption_mod_cast),
-  rwa ← real.coe_to_nnreal (abs x) (abs_nonneg x), assumption_mod_cast,
-end
+by rw [← pow_left_inj (abs_nonneg x) zero_le_one (pos_iff_ne_zero.2 hn), one_pow, pow_abs, h,
+  abs_one]
 
 theorem imo2008_q4
   (f : ℝ → ℝ)
diff --git a/src/algebra/group_power/lemmas.lean b/src/algebra/group_power/lemmas.lean
index ff4d3bea96dd3..b10adb48ee8c0 100644
--- a/src/algebra/group_power/lemmas.lean
+++ b/src/algebra/group_power/lemmas.lean
@@ -192,7 +192,7 @@ begin
   lift k to ℕ using int.le_of_lt hk,
   rw gsmul_coe_nat,
   apply nsmul_pos ha,
-  exact coe_nat_pos.mp hk,
+  exact (coe_nat_pos.mp hk).ne',
 end
 
 theorem gsmul_strict_mono_left {a : A} (ha : 0 < a) : strict_mono (λ n : ℤ, n • a) :=
diff --git a/src/algebra/group_power/order.lean b/src/algebra/group_power/order.lean
index 9bc1d0cb5105e..c6d689bc025af 100644
--- a/src/algebra/group_power/order.lean
+++ b/src/algebra/group_power/order.lean
@@ -13,82 +13,111 @@ Note that some lemmas are in `algebra/group_power/lemmas.lean` as they import fi
 depend on this file.
 -/
 
-variables {A R : Type*}
+variables {A G M R : Type*}
 
-section add_monoid
-variable [ordered_add_comm_monoid A]
+section preorder
 
-theorem nsmul_nonneg {a : A} (H : 0 ≤ a) : ∀ n : ℕ, 0 ≤ n • a
-| 0     := by rw [zero_nsmul]
-| (n+1) := by { rw succ_nsmul, exact add_nonneg H (nsmul_nonneg n) }
+variables [monoid M] [preorder M] [covariant_class M M (*) (≤)]
 
-lemma nsmul_pos {a : A} (ha : 0 < a) {k : ℕ} (hk : 0 < k) : 0 < k • a :=
+@[mono, to_additive nsmul_le_nsmul_of_le_right]
+lemma pow_le_pow_of_le_left' [covariant_class M M (function.swap (*)) (≤)]
+  {a b : M} (hab : a ≤ b) : ∀ i : ℕ, a ^ i ≤ b ^ i
+| 0     := by simp
+| (k+1) := by { rw [pow_succ, pow_succ],
+    exact mul_le_mul' hab (pow_le_pow_of_le_left' k) }
+
+@[to_additive nsmul_nonneg]
+theorem one_le_pow_of_one_le' {a : M} (H : 1 ≤ a) : ∀ n : ℕ, 1 ≤ a ^ n
+| 0       := by simp
+| (k + 1) := by { rw pow_succ, exact one_le_mul H (one_le_pow_of_one_le' k) }
+
+@[to_additive nsmul_nonpos]
+theorem pow_le_one' {a : M} (H : a ≤ 1) (n : ℕ) : a ^ n ≤ 1 :=
+@one_le_pow_of_one_le' (order_dual M) _ _ _ _ H n
+
+@[to_additive nsmul_le_nsmul]
+theorem pow_le_pow' {a : M} {n m : ℕ} (ha : 1 ≤ a) (h : n ≤ m) : a ^ n ≤ a ^ m :=
+let ⟨k, hk⟩ := nat.le.dest h in
+calc a ^ n ≤ a ^ n * a ^ k : le_mul_of_one_le_right' (one_le_pow_of_one_le' ha _)
+       ... = a ^ m         : by rw [← hk, pow_add]
+
+@[to_additive nsmul_le_nsmul_of_nonpos]
+theorem pow_le_pow_of_le_one' {a : M} {n m : ℕ} (ha : a ≤ 1) (h : n ≤ m) : a ^ m ≤ a ^ n :=
+@pow_le_pow' (order_dual M) _ _ _ _ _ _  ha h
+
+@[to_additive nsmul_pos]
+theorem one_lt_pow' {a : M} (ha : 1 < a) {k : ℕ} (hk : k ≠ 0) : 1 < a ^ k :=
 begin
-  rcases nat.exists_eq_succ_of_ne_zero (ne_of_gt hk) with ⟨l, rfl⟩,
+  rcases nat.exists_eq_succ_of_ne_zero hk with ⟨l, rfl⟩,
   clear hk,
   induction l with l IH,
   { simpa using ha },
-  { rw succ_nsmul,
-    exact add_pos ha IH }
+  { rw pow_succ,
+    exact one_lt_mul' ha IH }
 end
 
-theorem nsmul_le_nsmul {a : A} {n m : ℕ} (ha : 0 ≤ a) (h : n ≤ m) : n • a ≤ m • a :=
-let ⟨k, hk⟩ := nat.le.dest h in
-calc n • a = n • a + 0 : (add_zero _).symm
-  ... ≤ n • a + k • a : add_le_add_left (nsmul_nonneg ha _) _
-  ... = m • a : by rw [← hk, add_nsmul]
+@[to_additive nsmul_neg]
+theorem pow_lt_one' {a : M} (ha : a < 1) {k : ℕ} (hk : k ≠ 0) : a ^ k < 1 :=
+@one_lt_pow' (order_dual M) _ _ _ _ ha k hk
 
-lemma nsmul_le_nsmul_of_le_right {a b : A} (hab : a ≤ b) : ∀ i : ℕ, i • a ≤ i • b
-| 0 := by simp [zero_nsmul]
-| (k+1) := by { rw [succ_nsmul, succ_nsmul], exact add_le_add hab (nsmul_le_nsmul_of_le_right _) }
+@[to_additive nsmul_lt_nsmul]
+theorem pow_lt_pow'' [covariant_class M M (*) (<)] {a : M} {n m : ℕ} (ha : 1 < a) (h : n < m) :
+  a ^ n < a ^ m :=
+begin
+  rcases nat.le.dest h with ⟨k, rfl⟩, clear h,
+  rw [pow_add, pow_succ', mul_assoc, ← pow_succ],
+  exact lt_mul_of_one_lt_right' _ (one_lt_pow' ha k.succ_ne_zero)
+end
 
-end add_monoid
+end preorder
 
-section add_group
-variable [ordered_add_comm_group A]
+section linear_order
 
-theorem gsmul_nonneg {a : A} (H : 0 ≤ a) {n : ℤ} (hn : 0 ≤ n) :
-  0 ≤ n • a :=
-begin
-  lift n to ℕ using hn,
-  rw gsmul_coe_nat,
-  apply nsmul_nonneg H,
-end
+variables [monoid M] [linear_order M] [covariant_class M M (*) (≤)]
 
-end add_group
+@[to_additive nsmul_nonneg_iff]
+lemma one_le_pow_iff {x : M} {n : ℕ} (hn : n ≠ 0) : 1 ≤ x ^ n ↔ 1 ≤ x :=
+⟨le_imp_le_of_lt_imp_lt $ λ h, pow_lt_one' h hn, λ h, one_le_pow_of_one_le' h n⟩
 
-section cancel_add_monoid
-variable [ordered_cancel_add_comm_monoid A]
+@[to_additive nsmul_nonpos_iff]
+lemma pow_le_one_iff {x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n ≤ 1 ↔ x ≤ 1 :=
+@one_le_pow_iff (order_dual M) _ _ _ _ _ hn
 
-theorem nsmul_lt_nsmul {a : A} {n m : ℕ} (ha : 0 < a) (h : n < m) :
-  n • a < m • a :=
-let ⟨k, hk⟩ := nat.le.dest h in
+@[to_additive nsmul_pos_iff]
+lemma one_lt_pow_iff {x : M} {n : ℕ} (hn : n ≠ 0) : 1 < x ^ n ↔ 1 < x :=
+lt_iff_lt_of_le_iff_le (pow_le_one_iff hn)
+
+@[to_additive nsmul_neg_iff]
+lemma pow_lt_one_iff {x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n < 1 ↔ x < 1 :=
+lt_iff_lt_of_le_iff_le (one_le_pow_iff hn)
+
+@[to_additive nsmul_eq_zero_iff]
+lemma pow_eq_one_iff {x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n = 1 ↔ x = 1 :=
+by simp only [le_antisymm_iff, pow_le_one_iff hn, one_le_pow_iff hn]
+
+end linear_order
+
+section group
+
+variables [group G] [preorder G] [covariant_class G G (*) (≤)]
+
+@[to_additive gsmul_nonneg]
+theorem one_le_gpow {x : G} (H : 1 ≤ x) {n : ℤ} (hn : 0 ≤ n) :
+  1 ≤ x ^ n :=
 begin
-  have succ_swap : n.succ + k = n + k.succ := nat.succ_add n k,
-  calc n • a = (n • a : A) + (0 : A) : (add_zero _).symm
-    ... < n • a + (k.succ • a : A) : add_lt_add_left (nsmul_pos ha (nat.succ_pos k)) _
-    ... = m • a : by rw [← hk, succ_swap, add_nsmul]
+  lift n to ℕ using hn,
+  rw gpow_coe_nat,
+  apply one_le_pow_of_one_le' H,
 end
 
-end cancel_add_monoid
+end group
 
 namespace canonically_ordered_comm_semiring
-variable [canonically_ordered_comm_semiring R]
 
-theorem pow_pos {a : R} (H : 0 < a) : ∀ n : ℕ, 0 < a ^ n
-| 0     := by { nontriviality, rw pow_zero, exact zero_lt_one }
-| (n+1) := by { rw pow_succ, exact mul_pos.2 ⟨H, pow_pos n⟩ }
+variables [canonically_ordered_comm_semiring R]
 
-@[mono] lemma pow_le_pow_of_le_left {a b : R} (hab : a ≤ b) : ∀ i : ℕ, a^i ≤ b^i
-| 0     := by simp
-| (k+1) := by { rw [pow_succ, pow_succ],
-    exact mul_le_mul' hab (pow_le_pow_of_le_left k) }
-
-theorem one_le_pow_of_one_le {a : R} (H : 1 ≤ a) (n : ℕ) : 1 ≤ a ^ n :=
-by simpa only [one_pow] using pow_le_pow_of_le_left H n
-
-theorem pow_le_one {a : R} (H : a ≤ 1) (n : ℕ) : a ^ n ≤ 1:=
-by simpa only [one_pow] using pow_le_pow_of_le_left H n
+theorem pow_pos {a : R} (H : 0 < a) (n : ℕ) : 0 < a ^ n :=
+pos_iff_ne_zero.2 $ pow_ne_zero _ H.ne'
 
 end canonically_ordered_comm_semiring
 
@@ -169,9 +198,9 @@ end ordered_semiring
 section linear_ordered_semiring
 variable [linear_ordered_semiring R]
 
-theorem pow_left_inj {x y : R} {n : ℕ} (Hxpos : 0 ≤ x) (Hypos : 0 ≤ y) (Hnpos : 0 < n)
-  (Hxyn : x ^ n = y ^ n) : x = y :=
-(@strict_mono_incr_on_pow R _ _ Hnpos).inj_on Hxpos Hypos Hxyn
+@[simp] theorem pow_left_inj {x y : R} {n : ℕ} (Hxpos : 0 ≤ x) (Hypos : 0 ≤ y) (Hnpos : 0 < n) :
+  x ^ n = y ^ n ↔ x = y :=
+(@strict_mono_incr_on_pow R _ _ Hnpos).inj_on.eq_iff Hxpos Hypos
 
 lemma lt_of_pow_lt_pow {a b : R} (n : ℕ) (hb : 0 ≤ b) (h : a ^ n < b ^ n) : a < b :=
 lt_of_not_ge $ λ hn, not_lt_of_ge (pow_le_pow_of_le_left hb hn _) h
@@ -179,6 +208,9 @@ lt_of_not_ge $ λ hn, not_lt_of_ge (pow_le_pow_of_le_left hb hn _) h
 lemma le_of_pow_le_pow {a b : R} (n : ℕ) (hb : 0 ≤ b) (hn : 0 < n) (h : a ^ n ≤ b ^ n) : a ≤ b :=
 le_of_not_lt $ λ h1, not_le_of_lt (pow_lt_pow_of_lt_left h1 hb hn) h
 
+@[simp] lemma sq_eq_sq {a b : R} (ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ 2 = b ^ 2 ↔ a = b :=
+pow_left_inj ha hb dec_trivial
+
 end linear_ordered_semiring
 
 section linear_ordered_ring
@@ -256,16 +288,6 @@ end linear_ordered_ring
 section linear_ordered_comm_ring
 variables [linear_ordered_comm_ring R]
 
-@[simp] lemma eq_of_sq_eq_sq {a b : R} (ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ 2 = b ^ 2 ↔ a = b :=
-begin
-  refine ⟨_, congr_arg _⟩,
-  intros h,
-  refine (eq_or_eq_neg_of_sq_eq_sq _ _ h).elim id _,
-  rintros rfl,
-  rw le_antisymm (neg_nonneg.mp ha) hb,
-  exact neg_zero
-end
-
 /-- Arithmetic mean-geometric mean (AM-GM) inequality for linearly ordered commutative rings. -/
 lemma two_mul_le_add_sq (a b : R) : 2 * a * b ≤ a ^ 2 + b ^ 2 :=
 sub_nonneg.mp ((sub_add_eq_add_sub _ _ _).subst ((sub_sq a b).subst (sq_nonneg _)))
diff --git a/src/algebra/linear_ordered_comm_group_with_zero.lean b/src/algebra/linear_ordered_comm_group_with_zero.lean
index 236ed476f8f1c..1a3a2a19f91ee 100644
--- a/src/algebra/linear_ordered_comm_group_with_zero.lean
+++ b/src/algebra/linear_ordered_comm_group_with_zero.lean
@@ -73,57 +73,6 @@ def function.injective.linear_ordered_comm_monoid_with_zero {β : Type*}
   ..hf.ordered_comm_monoid f one mul,
   ..hf.comm_monoid_with_zero f zero one mul }
 
-lemma one_le_pow_of_one_le' {n : ℕ} (H : 1 ≤ x) : 1 ≤ x^n :=
-begin
-  induction n with n ih,
-  { rw pow_zero },
-  { rw pow_succ, exact one_le_mul H ih }
-end
-
-lemma pow_le_one_of_le_one {n : ℕ} (H : x ≤ 1) : x^n ≤ 1 :=
-begin
-  induction n with n ih,
-  { rw pow_zero },
-  { rw pow_succ, exact mul_le_one' H ih }
-end
-
-lemma eq_one_of_pow_eq_one {n : ℕ} (hn : n ≠ 0) (H : x ^ n = 1) : x = 1 :=
-begin
-  rcases nat.exists_eq_succ_of_ne_zero hn with ⟨n, rfl⟩, clear hn,
-  induction n with n ih,
-  { simpa using H },
-  { cases le_total x 1 with h,
-    all_goals
-    { have h1 := mul_le_mul_right' h (x ^ (n + 1)),
-      rw pow_succ at H,
-      rw [H, one_mul] at h1 },
-    { have h2 := pow_le_one_of_le_one h,
-      exact ih (le_antisymm h2 h1) },
-    { have h2 := one_le_pow_of_one_le' h,
-      exact ih (le_antisymm h1 h2) } }
-end
-
-lemma pow_eq_one_iff {n : ℕ} (hn : n ≠ 0) : x ^ n = 1 ↔ x = 1 :=
-⟨eq_one_of_pow_eq_one hn, by { rintro rfl, exact one_pow _ }⟩
-
-lemma one_le_pow_iff {n : ℕ} (hn : n ≠ 0) : 1 ≤ x^n ↔ 1 ≤ x :=
-begin
-  refine ⟨_, one_le_pow_of_one_le'⟩,
-  contrapose!,
-  intro h, apply lt_of_le_of_ne (pow_le_one_of_le_one (le_of_lt h)),
-  rw [ne.def, pow_eq_one_iff hn],
-  exact ne_of_lt h,
-end
-
-lemma pow_le_one_iff {n : ℕ} (hn : n ≠ 0) : x^n ≤ 1 ↔ x ≤ 1 :=
-begin
-  refine ⟨_, pow_le_one_of_le_one⟩,
-  contrapose!,
-  intro h, apply lt_of_le_of_ne (one_le_pow_of_one_le' (le_of_lt h)),
-  rw [ne.def, eq_comm, pow_eq_one_iff hn],
-  exact ne_of_gt h,
-end
-
 lemma zero_le_one' : (0 : α) ≤ 1 :=
 linear_ordered_comm_monoid_with_zero.zero_le_one
 
@@ -221,7 +170,7 @@ namespace monoid_hom
 variables {R : Type*} [ring R] (f : R →* α)
 
 theorem map_neg_one : f (-1) = 1 :=
-eq_one_of_pow_eq_one (nat.succ_ne_zero 1) $
+(pow_eq_one_iff (nat.succ_ne_zero 1)).1 $
   calc f (-1) ^ 2 = f (-1) * f(-1) : sq _
               ... = f ((-1) * - 1) : (f.map_mul _ _).symm
               ... = f ( - - 1)     : congr_arg _ (neg_one_mul _)
diff --git a/src/analysis/normed_space/inner_product.lean b/src/analysis/normed_space/inner_product.lean
index 272599124a2c7..979dd9adaa1d5 100644
--- a/src/analysis/normed_space/inner_product.lean
+++ b/src/analysis/normed_space/inner_product.lean
@@ -692,8 +692,8 @@ begin
     { intros i,
       have h' : ∥v i∥ ^ 2 = 1 ^ 2 := by simp [norm_sq_eq_inner, h i i],
       have h₁ : 0 ≤ ∥v i∥ := norm_nonneg _,
-      have h₂ : (0:ℝ) ≤ 1 := by norm_num,
-      rwa eq_of_sq_eq_sq h₁ h₂ at h' },
+      have h₂ : (0:ℝ) ≤ 1 := zero_le_one,
+      rwa sq_eq_sq h₁ h₂ at h' },
     { intros i j hij,
       simpa [hij] using h i j } }
 end
diff --git a/src/analysis/specific_limits.lean b/src/analysis/specific_limits.lean
index 7f8d37c64b3b1..ec155fc5527d9 100644
--- a/src/analysis/specific_limits.lean
+++ b/src/analysis/specific_limits.lean
@@ -404,10 +404,8 @@ begin
   { rw [ennreal.sub_eq_zero_of_le hr, ennreal.inv_zero, ennreal.tsum_eq_supr_nat, supr_eq_top],
     refine λ a ha, (ennreal.exists_nat_gt (lt_top_iff_ne_top.1 ha)).imp
       (λ n hn, lt_of_lt_of_le hn _),
-    have : ∀ k:ℕ, 1 ≤ r^k,
-      by simpa using canonically_ordered_comm_semiring.pow_le_pow_of_le_left hr,
-    calc (n:ℝ≥0∞) = (∑ i in range n, 1) : by rw [sum_const, nsmul_one, card_range]
-    ... ≤ ∑ i in range n, r ^ i : sum_le_sum (λ k _, this k) }
+    calc (n:ℝ≥0∞) = ∑ i in range n, 1     : by rw [sum_const, nsmul_one, card_range]
+              ... ≤ ∑ i in range n, r ^ i : sum_le_sum (λ k _, one_le_pow_of_one_le' hr k) }
 end
 
 variables {K : Type*} [normed_field K] {ξ : K}
diff --git a/src/data/nat/basic.lean b/src/data/nat/basic.lean
index 3ad34f45155ff..ce325b48e8dfd 100644
--- a/src/data/nat/basic.lean
+++ b/src/data/nat/basic.lean
@@ -71,6 +71,8 @@ instance : linear_ordered_comm_monoid_with_zero ℕ :=
   ..nat.linear_ordered_semiring,
   ..(infer_instance : comm_monoid_with_zero ℕ)}
 
+instance : ordered_comm_semiring ℕ := { .. nat.comm_semiring, .. nat.linear_ordered_semiring }
+
 /-! Extra instances to short-circuit type class resolution -/
 instance : add_comm_monoid nat    := by apply_instance
 instance : add_monoid nat         := by apply_instance
diff --git a/src/data/nat/pow.lean b/src/data/nat/pow.lean
index 56a9729f78cd5..f832b2d95e2c1 100644
--- a/src/data/nat/pow.lean
+++ b/src/data/nat/pow.lean
@@ -15,40 +15,23 @@ namespace nat
 
 /-! ### `pow` -/
 
--- This is redundant with `canonically_ordered_comm_semiring.pow_le_pow_of_le_left`,
--- but `canonically_ordered_comm_semiring` is not such an obvious abstraction, and also quite long.
--- So, we leave a version in the `nat` namespace as well.
+-- This is redundant with `pow_le_pow_of_le_left'`,
+-- We leave a version in the `nat` namespace as well.
 -- (The global `pow_le_pow_of_le_left` needs an extra hypothesis `0 ≤ x`.)
 protected theorem pow_le_pow_of_le_left {x y : ℕ} (H : x ≤ y) : ∀ i : ℕ, x^i ≤ y^i :=
-canonically_ordered_comm_semiring.pow_le_pow_of_le_left H
+pow_le_pow_of_le_left' H
 
-theorem pow_le_pow_of_le_right {x : ℕ} (H : x > 0) {i : ℕ} : ∀ {j}, i ≤ j → x^i ≤ x^j
-| 0        h := by rw nat.eq_zero_of_le_zero h; apply le_refl
-| (succ j) h := h.lt_or_eq_dec.elim
-  (λhl, by rw [pow_succ', ← nat.mul_one (x^i)]; exact
-    nat.mul_le_mul (pow_le_pow_of_le_right $ le_of_lt_succ hl) H)
-  (λe, by rw e; refl)
+theorem pow_le_pow_of_le_right {x : ℕ} (H : 0 < x) {i j : ℕ} (h : i ≤ j) : x ^ i ≤ x ^ j :=
+pow_le_pow' H h
 
 theorem pow_lt_pow_of_lt_left {x y : ℕ} (H : x < y) {i} (h : 0 < i) : x^i < y^i :=
-begin
-  cases i with i, { exact absurd h (nat.not_lt_zero _) },
-  rw [pow_succ', pow_succ'],
-  exact nat.mul_lt_mul' (nat.pow_le_pow_of_le_left (le_of_lt H) _) H
-    (pow_pos (lt_of_le_of_lt (zero_le _) H) _)
-end
+pow_lt_pow_of_lt_left H (zero_le _) h
 
-theorem pow_lt_pow_of_lt_right {x : ℕ} (H : x > 1) {i j : ℕ} (h : i < j) : x^i < x^j :=
-begin
-  have xpos := lt_of_succ_lt H,
-  refine lt_of_lt_of_le _ (pow_le_pow_of_le_right xpos h),
-  rw [← nat.mul_one (x^i), pow_succ'],
-  exact nat.mul_lt_mul_of_pos_left H (pow_pos xpos _)
-end
+theorem pow_lt_pow_of_lt_right {x : ℕ} (H : 1 < x) {i j : ℕ} (h : i < j) : x^i < x^j :=
+pow_lt_pow H h
 
--- TODO: Generalize?
 lemma pow_lt_pow_succ {p : ℕ} (h : 1 < p) (n : ℕ) : p^n < p^(n+1) :=
-suffices 1*p^n < p*p^n, by simpa [pow_succ],
-nat.mul_lt_mul_of_pos_right h (pow_pos (lt_of_succ_lt h) n)
+pow_lt_pow_of_lt_right h n.lt_succ_self
 
 lemma lt_pow_self {p : ℕ} (h : 1 < p) : ∀ n : ℕ, n < p ^ n
 | 0 := by simp [zero_lt_one]
@@ -133,8 +116,8 @@ alias nat.sq_sub_sq ← nat.pow_two_sub_pow_two
 
 /-! ### `pow` and `mod` / `dvd` -/
 
-theorem mod_pow_succ {b : ℕ} (b_pos : 0 < b) (w m : ℕ)
-: m % (b^succ w) = b * (m/b % b^w) + m % b :=
+theorem mod_pow_succ {b : ℕ} (b_pos : 0 < b) (w m : ℕ) :
+  m % (b^succ w) = b * (m/b % b^w) + m % b :=
 begin
   apply nat.strong_induction_on m,
   clear m,
diff --git a/src/data/real/nnreal.lean b/src/data/real/nnreal.lean
index 3796090a1debf..973b73a881ddd 100644
--- a/src/data/real/nnreal.lean
+++ b/src/data/real/nnreal.lean
@@ -111,7 +111,12 @@ nnreal.coe_injective.eq_iff
 max_eq_left $ le_sub.2 $ by simp [show (r₂ : ℝ) ≤ r₁, from h]
 
 -- TODO: setup semifield!
-@[simp] protected lemma coe_eq_zero (r : ℝ≥0) : ↑r = (0 : ℝ) ↔ r = 0 := by norm_cast
+@[simp, norm_cast] protected lemma coe_eq_zero (r : ℝ≥0) : ↑r = (0 : ℝ) ↔ r = 0 :=
+by rw [← nnreal.coe_zero, nnreal.coe_eq]
+
+@[simp, norm_cast] protected lemma coe_eq_one (r : ℝ≥0) : ↑r = (1 : ℝ) ↔ r = 1 :=
+by rw [← nnreal.coe_one, nnreal.coe_eq]
+
 lemma coe_ne_zero {r : ℝ≥0} : (r : ℝ) ≠ 0 ↔ r ≠ 0 := by norm_cast
 
 instance : comm_semiring ℝ≥0 :=
diff --git a/src/geometry/euclidean/basic.lean b/src/geometry/euclidean/basic.lean
index 52920cdbbc0db..408410d4b3160 100644
--- a/src/geometry/euclidean/basic.lean
+++ b/src/geometry/euclidean/basic.lean
@@ -294,7 +294,7 @@ end
 the sum of their norms. -/
 lemma norm_sub_eq_add_norm_of_angle_eq_pi {x y : V} (h : angle x y = π) : ∥x - y∥ = ∥x∥ + ∥y∥ :=
 begin
-  rw ← eq_of_sq_eq_sq (norm_nonneg (x - y)) (add_nonneg (norm_nonneg x) (norm_nonneg y)),
+  rw ← sq_eq_sq (norm_nonneg (x - y)) (add_nonneg (norm_nonneg x) (norm_nonneg y)),
   rw [norm_sub_pow_two_real, inner_eq_neg_mul_norm_of_angle_eq_pi h],
   ring,
 end
@@ -303,7 +303,7 @@ end
 the sum of their norms. -/
 lemma norm_add_eq_add_norm_of_angle_eq_zero {x y : V} (h : angle x y = 0) : ∥x + y∥ = ∥x∥ + ∥y∥ :=
 begin
-  rw ← eq_of_sq_eq_sq (norm_nonneg (x + y)) (add_nonneg (norm_nonneg x) (norm_nonneg y)),
+  rw ← sq_eq_sq (norm_nonneg (x + y)) (add_nonneg (norm_nonneg x) (norm_nonneg y)),
   rw [norm_add_pow_two_real, inner_eq_mul_norm_of_angle_eq_zero h],
   ring,
 end
@@ -313,7 +313,7 @@ the absolute value of the difference of their norms. -/
 lemma norm_sub_eq_abs_sub_norm_of_angle_eq_zero {x y : V} (h : angle x y = 0) :
   ∥x - y∥ = abs (∥x∥ - ∥y∥) :=
 begin
-  rw [← eq_of_sq_eq_sq (norm_nonneg (x - y)) (abs_nonneg (∥x∥ - ∥y∥)),
+  rw [← sq_eq_sq (norm_nonneg (x - y)) (abs_nonneg (∥x∥ - ∥y∥)),
       norm_sub_pow_two_real, inner_eq_mul_norm_of_angle_eq_zero h, sq_abs (∥x∥ - ∥y∥)],
   ring,
 end
@@ -326,7 +326,7 @@ begin
   refine ⟨λ h, _, norm_sub_eq_add_norm_of_angle_eq_pi⟩,
   rw ← inner_eq_neg_mul_norm_iff_angle_eq_pi hx hy,
   obtain ⟨hxy₁, hxy₂⟩ := ⟨norm_nonneg (x - y), add_nonneg (norm_nonneg x) (norm_nonneg y)⟩,
-  rw [← eq_of_sq_eq_sq hxy₁ hxy₂, norm_sub_pow_two_real] at h,
+  rw [← sq_eq_sq hxy₁ hxy₂, norm_sub_pow_two_real] at h,
   calc inner x y = (∥x∥ ^ 2 + ∥y∥ ^ 2 - (∥x∥ + ∥y∥) ^ 2) / 2 : by linarith
   ...            = -(∥x∥ * ∥y∥) : by ring,
 end
@@ -339,7 +339,7 @@ begin
   refine ⟨λ h, _, norm_add_eq_add_norm_of_angle_eq_zero⟩,
   rw ← inner_eq_mul_norm_iff_angle_eq_zero hx hy,
   obtain ⟨hxy₁, hxy₂⟩ := ⟨norm_nonneg (x + y), add_nonneg (norm_nonneg x) (norm_nonneg y)⟩,
-  rw [← eq_of_sq_eq_sq hxy₁ hxy₂, norm_add_pow_two_real] at h,
+  rw [← sq_eq_sq hxy₁ hxy₂, norm_add_pow_two_real] at h,
   calc inner x y = ((∥x∥ + ∥y∥) ^ 2 - ∥x∥ ^ 2 - ∥y∥ ^ 2)/ 2 : by linarith
   ...            = ∥x∥ * ∥y∥ : by ring,
 end
@@ -362,7 +362,7 @@ the angle between them is π/2. -/
 lemma norm_add_eq_norm_sub_iff_angle_eq_pi_div_two (x y : V) :
   ∥x + y∥ = ∥x - y∥ ↔ angle x y = π / 2 :=
 begin
-  rw [← eq_of_sq_eq_sq (norm_nonneg (x + y)) (norm_nonneg (x - y)),
+  rw [← sq_eq_sq (norm_nonneg (x + y)) (norm_nonneg (x - y)),
       ← inner_eq_zero_iff_angle_eq_pi_div_two x y, norm_add_pow_two_real, norm_sub_pow_two_real],
   split; intro h; linarith,
 end
diff --git a/src/geometry/euclidean/sphere.lean b/src/geometry/euclidean/sphere.lean
index fa07f45142b6a..a9d1680a5aee6 100644
--- a/src/geometry/euclidean/sphere.lean
+++ b/src/geometry/euclidean/sphere.lean
@@ -68,9 +68,8 @@ begin
     ... = 0                         : sub_eq_zero.mpr hk.symm },
 
   have hzy : ⟪z, y⟫ = 0,
-  { rw [← eq_of_sq_eq_sq (norm_nonneg (z - y)) (norm_nonneg (z + y)),
-        norm_add_sq_real, norm_sub_sq_real] at h₂,
-    linarith },
+    by rwa [inner_eq_zero_iff_angle_eq_pi_div_two, ← norm_add_eq_norm_sub_iff_angle_eq_pi_div_two,
+      eq_comm],
 
   have hzx : ⟪z, x⟫ = 0 := by rw [hxy, inner_smul_right, hzy, mul_zero],
 
diff --git a/src/geometry/euclidean/triangle.lean b/src/geometry/euclidean/triangle.lean
index 099b2de64d7ef..de58f1b6cc0ff 100644
--- a/src/geometry/euclidean/triangle.lean
+++ b/src/geometry/euclidean/triangle.lean
@@ -398,7 +398,7 @@ begin
     rw [hab₁, hab'₁, dist_comm b' c', dist_comm b c, hcb] },
   { have h1 : 0 ≤ r * dist a b, { rw ← hab, exact dist_nonneg },
     have h2 : 0 ≤ r := nonneg_of_mul_nonneg_right h1 (dist_pos.mpr hab₁),
-    exact (eq_of_sq_eq_sq dist_nonneg (mul_nonneg h2 dist_nonneg)).mp h' },
+    exact (sq_eq_sq dist_nonneg (mul_nonneg h2 dist_nonneg)).mp h' },
 end
 
 end euclidean_geometry
diff --git a/src/measure_theory/measure/hausdorff.lean b/src/measure_theory/measure/hausdorff.lean
index 4360195bf27f3..3e41283db6129 100644
--- a/src/measure_theory/measure/hausdorff.lean
+++ b/src/measure_theory/measure/hausdorff.lean
@@ -761,7 +761,7 @@ begin
       assume n hn,
       apply finset.sum_le_sum (λ i _, _),
       rw ennreal.rpow_nat_cast,
-      exact canonically_ordered_comm_semiring.pow_le_pow_of_le_left (hn i) _,
+      exact pow_le_pow_of_le_left' (hn i) _,
     end
   ... = liminf at_top (λ (n : ℕ), ∏ (i : ι), (⌈((b i : ℝ) - a i) * n⌉₊ : ℝ≥0∞) / n) :
   begin
diff --git a/src/ring_theory/perfection.lean b/src/ring_theory/perfection.lean
index dbae95179f92c..463c829f91c29 100644
--- a/src/ring_theory/perfection.lean
+++ b/src/ring_theory/perfection.lean
@@ -518,8 +518,8 @@ begin
   rw [val_aux_eq hm, val_aux_eq hn, val_aux_eq hk, ring_hom.map_add],
   cases le_max_iff.1
     (mod_p.pre_val_add (coeff _ _ (max (max m n) k) f) (coeff _ _ (max (max m n) k) g)) with h h,
-  { exact le_max_of_le_left (canonically_ordered_comm_semiring.pow_le_pow_of_le_left h _) },
-  { exact le_max_of_le_right (canonically_ordered_comm_semiring.pow_le_pow_of_le_left h _) }
+  { exact le_max_of_le_left (pow_le_pow_of_le_left' h _) },
+  { exact le_max_of_le_right (pow_le_pow_of_le_left' h _) }
 end
 
 variables (K v O hv p)
diff --git a/src/ring_theory/valuation/integral.lean b/src/ring_theory/valuation/integral.lean
index f7e8931e010cf..45f7e00eca27c 100644
--- a/src/ring_theory/valuation/integral.lean
+++ b/src/ring_theory/valuation/integral.lean
@@ -34,17 +34,15 @@ let ⟨p, hpm, hpx⟩ := hx in le_of_not_lt $ λ hvx, begin
   rw [hpm.as_sum, eval₂_add, eval₂_pow, eval₂_X, eval₂_finset_sum, add_eq_zero_iff_eq_neg] at hpx,
   replace hpx := congr_arg v hpx, refine ne_of_gt _ hpx,
   rw [v.map_neg, v.map_pow],
-  refine v.map_sum_lt' (lt_of_lt_of_le (lt_of_le_of_ne zero_le_one' zero_ne_one)
-      (one_le_pow_of_one_le' $ le_of_lt hvx))
-    (λ i hi, _),
+  refine v.map_sum_lt' (zero_lt_one''.trans_le (one_le_pow_of_one_le' hvx.le _)) (λ i hi, _),
   rw [eval₂_mul, eval₂_pow, eval₂_C, eval₂_X, v.map_mul, v.map_pow, ← one_mul (v x ^ p.nat_degree)],
-  cases lt_or_eq_of_le (hv.2 $ p.coeff i) with hvpi hvpi,
+  cases (hv.2 $ p.coeff i).lt_or_eq with hvpi hvpi,
   { exact mul_lt_mul'''' hvpi (pow_lt_pow' hvx $ finset.mem_range.1 hi) },
   { erw hvpi, rw [one_mul, one_mul], exact pow_lt_pow' hvx (finset.mem_range.1 hi) }
 end
 
 protected lemma integral_closure : integral_closure O R = ⊥ :=
-eq_bot_iff.2 $ λ r hr, let ⟨x, hx⟩ := hv.3 (hv.mem_of_integral hr) in algebra.mem_bot.2 ⟨x, hx⟩
+bot_unique $ λ r hr, let ⟨x, hx⟩ := hv.3 (hv.mem_of_integral hr) in algebra.mem_bot.2 ⟨x, hx⟩
 
 end comm_ring