refactor(algebra/group_power): use covariant_class (#8713)

## Main changes

* use `covariant_class` instead of `canonically_ordered_*` or `ordered_add_*` as an assumption in many lemmas;
* move some lemmas to the root namespace;
* use `to_additive` for more lemmas;

## Detailed list of API changes

* `canonically_ordered_comm_semiring.pow_le_pow_of_le_left`:
  - rename to `pow_le_pow_of_le_left'`;
  - assume `[covariant_class M M (*) (≤)]`;
  - use `to_additive` to generate `nsmul_le_nsmul_of_le_right`;
* `canonically_ordered_comm_semiring.one_le_pow_of_one_le`:
  - rename to `one_le_pow_of_one_le`';
  - assume `[covariant_class M M (*) (≤)]`;
  - use `to_additive` to generate `nsmul_nonneg`;
* `canonically_ordered_comm_semiring.pow_le_one`:
  - rename to `pow_le_one'`;
  - assume `[covariant_class M M (*) (≤)]`;
  - use `to_additive` to generate `nsmul_nonpos`;
* add `pow_le_pow'`, generate `nsmul_le_nsmul`;
* add `pow_le_pow_of_le_one'` and `nsmul_le_nsmul_of_nonpos`;
* add `one_lt_pow'`, generate `nsmul_pos`;
  - as a side effect, `nsmul_pos` now assumes `n ≠ 0` instead of `0 < n`.
* add `pow_lt_one'`, generate `nsmul_neg`;
* add `pow_lt_pow'`, generate `nsmul_lt_nsmul`;
* generalize `one_le_pow_iff` and `pow_le_one_iff`, generate `nsmul_nonneg_iff` and `nsmul_nonpos_iff`;
* generalize `one_lt_pow_iff`, `pow_lt_one_iff`, and `pow_eq_one_iff`, generate `nsmul_pos_iff`, `nsmul_neg_iff`, and `nsmul_eq_zero_iff`;
* add `one_le_gpow`, generate `gsmul_nonneg`;
* rename `eq_of_sq_eq_sq` to `sq_eq_sq`, golf;
* drop `eq_one_of_pow_eq_one` in favor of the `iff` version `pow_eq_one_iff`;
* add missing instance `nat.ordered_comm_semiring`;

## Misc changes

* replace some proofs about `nat.pow` with references to generic lemmas;
* add `nnreal.coe_eq_one`;

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 : ℝ → ℝ)

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) :=

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,16 +198,19 @@ 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
 
 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 _)))

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 _)

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

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}

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

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,