feat(algebra/order/ring): Non-cancellative ordered semirings (#16172)

## Historical background

This tackles a problem that we have had for six years (#2697 for its move to mathlib, before it was in core): `ordered_semiring` assumes that addition and multiplication are strictly monotone.

This led to weirdness within the algebraic order hierarchy:
* `ennreal`/`ereal`/`enat` needed custom lemmas (`∞ + 0 = ∞ = ∞ + 1`, `1 * ∞ = ∞ = 2 * ∞`).
* A `canonically_ordered_comm_semiring` was not an `ordered_comm_semiring`!

## What this PR does

This PR solves the problem minimally by renaming `ordered_(comm_)semiring` to `strict_ordered_(comm_)semiring` and adding a new class `ordered_(comm_)semiring` that doesn't assume strict monotonicity of addition and multiplication but only monotonicity:
```
class ordered_semiring (α : Type*) extends semiring α, ordered_add_comm_monoid α :=
(zero_le_one : (0 : α) ≤ 1)
(mul_le_mul_of_nonneg_left  : ∀ a b c : α, a ≤ b → 0 ≤ c → c * a ≤ c * b)
(mul_le_mul_of_nonneg_right : ∀ a b c : α, a ≤ b → 0 ≤ c → a * c ≤ b * c)

class ordered_comm_semiring (α : Type*) extends ordered_semiring α, comm_semiring α

class ordered_ring (α : Type u) extends ring α, ordered_add_comm_group α :=
(zero_le_one : 0 ≤ (1 : α))
(mul_nonneg : ∀ a b : α, 0 ≤ a → 0 ≤ b → 0 ≤ a * b)

class ordered_comm_ring (α : Type u) extends ordered_ring α, comm_ring α

class strict_ordered_semiring (α : Type*) extends semiring α, ordered_cancel_add_comm_monoid α :=
(zero_le_one : (0 : α) ≤ 1)
(mul_lt_mul_of_pos_left  : ∀ a b c : α, a < b → 0 < c → c * a < c * b)
(mul_lt_mul_of_pos_right : ∀ a b c : α, a < b → 0 < c → a * c < b * c)

class strict_ordered_comm_semiring (α : Type*) extends strict_ordered_semiring α, comm_semiring α

class strict_ordered_ring (α : Type u) extends ring α, ordered_add_comm_group α :=
(zero_le_one : 0 ≤ (1 : α))
(mul_pos     : ∀ a b : α, 0 < a → 0 < b → 0 < a * b)

class strict_ordered_comm_ring (α : Type*) extends strict_ordered_ring α, comm_ring α
```

## Whatever happened to the `decidable` lemmas?

Scrolling through the diff, you will see that only one lemma in the `decidable` namespace out of many survives this PR. Those lemmas were originally meant to avoid using choice in the proof of `nat` and `int` lemmas.

The need for decidability originated from the proofs of `mul_le_mul_of_nonneg_left`/`mul_le_mul_of_nonneg_right`.
```
protected lemma decidable.mul_le_mul_of_nonneg_left [@decidable_rel α (≤)]
  (h₁ : a ≤ b) (h₂ : 0 ≤ c) : c * a ≤ c * b :=
begin
  by_cases ba : b ≤ a, { simp [ba.antisymm h₁] },
  by_cases c0 : c ≤ 0, { simp [c0.antisymm h₂] },
  exact (mul_lt_mul_of_pos_left (h₁.lt_of_not_le ba) (h₂.lt_of_not_le c0)).le,
end
```
Now that these are fields to `ordered_semiring`, they are already choice-free. Instead, choice is now used in showing that an `ordered_cancel_semiring` is an `ordered_semiring`.
```
@[priority 100] -- see Note [lower instance priority]
instance ordered_cancel_semiring.to_ordered_semiring : ordered_semiring α :=
{ mul_le_mul_of_nonneg_left := λ a b c hab hc, begin
    obtain rfl | hab := hab.eq_or_lt,
    { refl },
    obtain rfl | hc := hc.eq_or_lt,
    { simp },
    { exact (mul_lt_mul_of_pos_left hab hc).le }
  end,
  mul_le_mul_of_nonneg_right := λ a b c hab hc, begin
    obtain rfl | hab := hab.eq_or_lt,
    { refl },
    obtain rfl | hc := hc.eq_or_lt,
    { simp },
    { exact (mul_lt_mul_of_pos_right hab hc).le }
  end,
  ..‹ordered_cancel_semiring α› }
```
It seems unreasonable to make that instance depend on `@decidable_rel α (≤)` even though it's only needed for the proofs.

## Other changes

To have some lemmas in the generality of the new `ordered_semiring`, I needed a few new lemmas:
* `bit0_mono`
* `bit0_strict_mono`

It was also simpler to golf `analysis.special_functions.stirling` using `positivity` rather than fixing it so I introduce the following (simple) `positivity` extensions:
* `positivity_succ`
* `positivity_factorial`
* `positivity_asc_factorial`

archive/imo/imo2008_q3.lean

@@ -66,11 +66,11 @@ begin
   have hreal₃ : (k:ℝ) ^ 2 + 4 ≥ p, { assumption_mod_cast },
 
   have hreal₅ : (k:ℝ) > 4,
-  { apply lt_of_pow_lt_pow 2 k.cast_nonneg,
+  { refine lt_of_pow_lt_pow 2 k.cast_nonneg _,
     linarith only [hreal₂, hreal₃] },
 
   have hreal₆ : (k:ℝ) > sqrt (2 * n),
-  { apply lt_of_pow_lt_pow 2 k.cast_nonneg,
+  { refine lt_of_pow_lt_pow 2 k.cast_nonneg _,
     rw sq_sqrt (mul_nonneg zero_le_two n.cast_nonneg),
     linarith only [hreal₁, hreal₃, hreal₅] },
 

counterexamples/canonically_ordered_comm_semiring_two_mul.lean

@@ -132,7 +132,7 @@ lemma mul_lt_mul_of_pos_left : ∀ (a b c : ℕ × zmod 2), a < b → 0 < c →
 lemma mul_lt_mul_of_pos_right : ∀ (a b c : ℕ × zmod 2), a < b → 0 < c → a * c < b * c :=
 λ a b c ab c0, lt_def.mpr ((mul_lt_mul_right (lt_def.mp c0)).mpr (lt_def.mp ab))
 
-instance ocsN2 : ordered_comm_semiring (ℕ × zmod 2) :=
+instance socsN2 : strict_ordered_comm_semiring (ℕ × zmod 2) :=
 { add_le_add_left := add_le_add_left,
   le_of_add_le_add_left := le_of_add_le_add_left,
   zero_le_one := zero_le_one,

src/algebra/algebra/subalgebra/basic.lean

@@ -188,9 +188,15 @@ instance to_comm_ring {R A}
 instance to_ordered_semiring {R A}
   [comm_semiring R] [ordered_semiring A] [algebra R A] (S : subalgebra R A) :
   ordered_semiring S := S.to_subsemiring.to_ordered_semiring
+instance to_strict_ordered_semiring {R A}
+  [comm_semiring R] [strict_ordered_semiring A] [algebra R A] (S : subalgebra R A) :
+  strict_ordered_semiring S := S.to_subsemiring.to_strict_ordered_semiring
 instance to_ordered_comm_semiring {R A}
   [comm_semiring R] [ordered_comm_semiring A] [algebra R A] (S : subalgebra R A) :
   ordered_comm_semiring S := S.to_subsemiring.to_ordered_comm_semiring
+instance to_strict_ordered_comm_semiring {R A}
+  [comm_semiring R] [strict_ordered_comm_semiring A] [algebra R A] (S : subalgebra R A) :
+  strict_ordered_comm_semiring S := S.to_subsemiring.to_strict_ordered_comm_semiring
 instance to_ordered_ring {R A}
   [comm_ring R] [ordered_ring A] [algebra R A] (S : subalgebra R A) :
   ordered_ring S := S.to_subring.to_ordered_ring

src/algebra/big_operators/order.lean

@@ -411,6 +411,14 @@ lt_of_le_of_lt (by rw prod_const_one) $ prod_lt_prod_of_nonempty' hs h
   (∏ i in s, f i) < 1 :=
 (prod_lt_prod_of_nonempty' hs h).trans_le (by rw prod_const_one)
 
+@[to_additive sum_pos'] lemma one_lt_prod' (h : ∀ i ∈ s, 1 ≤ f i) (hs : ∃ i ∈ s, 1 < f i) :
+  1 < (∏ i in s, f i) :=
+prod_const_one.symm.trans_lt $ prod_lt_prod' h hs
+
+@[to_additive] lemma prod_lt_one' (h : ∀ i ∈ s, f i ≤ 1) (hs : ∃ i ∈ s, f i < 1)  :
+  ∏ i in s, f i < 1 :=
+prod_const_one.le.trans_lt' $ prod_lt_prod' h hs
+
 @[to_additive] lemma prod_eq_prod_iff_of_le {f g : ι → M} (h : ∀ i ∈ s, f i ≤ g i) :
   ∏ i in s, f i = ∏ i in s, g i ↔ ∀ i ∈ s, f i = g i :=
 begin
@@ -464,15 +472,10 @@ section ordered_comm_semiring
 variables [ordered_comm_semiring R] {f g : ι → R} {s t : finset ι}
 open_locale classical
 
-/- this is also true for a ordered commutative multiplicative monoid -/
+/- this is also true for a ordered commutative multiplicative monoid with zero -/
 lemma prod_nonneg (h0 : ∀ i ∈ s, 0 ≤ f i) : 0 ≤ ∏ i in s, f i :=
 prod_induction f (λ i, 0 ≤ i) (λ _ _ ha hb, mul_nonneg ha hb) zero_le_one h0
 
-/- this is also true for a ordered commutative multiplicative monoid -/
-lemma prod_pos [nontrivial R] (h0 : ∀ i ∈ s, 0 < f i) :
-  0 < ∏ i in s, f i :=
-prod_induction f (λ x, 0 < x) (λ _ _ ha hb, mul_pos ha hb) zero_lt_one h0
-
 /-- If all `f i`, `i ∈ s`, are nonnegative and each `f i` is less than or equal to `g i`, then the
 product of `f i` is less than or equal to the product of `g i`. See also `finset.prod_le_prod''` for
 the case of an ordered commutative multiplicative monoid. -/
@@ -515,6 +518,15 @@ end
 
 end ordered_comm_semiring
 
+section strict_ordered_comm_semiring
+variables [strict_ordered_comm_semiring R] [nontrivial R] {f : ι → R} {s : finset ι}
+
+/- This is also true for a ordered commutative multiplicative monoid with zero -/
+lemma prod_pos (h0 : ∀ i ∈ s, 0 < f i) : 0 < ∏ i in s, f i :=
+prod_induction f (λ x, 0 < x) (λ _ _ ha hb, mul_pos ha hb) zero_lt_one h0
+
+end strict_ordered_comm_semiring
+
 section canonically_ordered_comm_semiring
 
 variables [canonically_ordered_comm_semiring R] {f g h : ι → R} {s : finset ι} {i : ι}

src/algebra/geom_sum.lean

@@ -409,10 +409,11 @@ section order
 
 variables {n : ℕ} {x : α}
 
-lemma geom_sum_pos [ordered_semiring α] (hx : 0 < x) (hn : n ≠ 0) : 0 < ∑ i in range n, x ^ i :=
-sum_pos (λ k hk, pow_pos hx _) $ nonempty_range_iff.2 hn
+lemma geom_sum_pos [strict_ordered_semiring α] [nontrivial α] (hx : 0 ≤ x) (hn : n ≠ 0) :
+  0 < ∑ i in range n, x ^ i :=
+sum_pos' (λ k hk, pow_nonneg hx _) ⟨0, mem_range.2 hn.bot_lt, by simp⟩
 
-lemma geom_sum_pos_and_lt_one [ordered_ring α] (hx : x < 0) (hx' : 0 < x + 1) (hn : 1 < n) :
+lemma geom_sum_pos_and_lt_one [strict_ordered_ring α] (hx : x < 0) (hx' : 0 < x + 1) (hn : 1 < n) :
   0 < ∑ i in range n, x ^ i ∧ ∑ i in range n, x ^ i < 1 :=
 begin
   refine nat.le_induction _ _ n (show 2 ≤ n, from hn),
@@ -425,7 +426,22 @@ begin
     (neg_lt_iff_pos_add'.2 hx') ihn.2.le, mul_neg_of_neg_of_pos hx ihn.1⟩
 end
 
-lemma geom_sum_alternating_of_lt_neg_one [ordered_ring α] (hx : x + 1 < 0) (hn : 1 < n) :
+lemma geom_sum_alternating_of_le_neg_one [strict_ordered_ring α] (hx : x + 1 ≤ 0) (n : ℕ) :
+  if even n then ∑ i in range n, x ^ i ≤ 0 else 1 ≤ ∑ i in range n, x ^ i :=
+begin
+  have hx0 : x ≤ 0 := (le_add_of_nonneg_right zero_le_one).trans hx,
+  induction n with n ih,
+  { simp only [even_zero, geom_sum_zero, le_refl] },
+  simp only [nat.even_add_one, geom_sum_succ],
+  split_ifs at ih,
+  { rw [if_neg (not_not_intro h), le_add_iff_nonneg_left],
+    exact mul_nonneg_of_nonpos_of_nonpos hx0 ih },
+  { rw if_pos h,
+    refine (add_le_add_right _ _).trans hx,
+    simpa only [mul_one] using mul_le_mul_of_nonpos_left ih hx0 }
+end
+
+lemma geom_sum_alternating_of_lt_neg_one [strict_ordered_ring α] (hx : x + 1 < 0) (hn : 1 < n) :
   if even n then ∑ i in range n, x ^ i < 0 else 1 < ∑ i in range n, x ^ i  :=
 begin
   have hx0 : x < 0, from ((le_add_iff_nonneg_right _).2 zero_le_one).trans_lt hx,
@@ -443,6 +459,17 @@ begin
     exact this.trans hx }
 end
 
+lemma geom_sum_pos' [linear_ordered_ring α] (hx : 0 < x + 1) (hn : n ≠ 0) :
+  0 < ∑ i in range n, x ^ i :=
+begin
+  obtain _ | _ | n := n,
+  { cases hn rfl },
+  { simp },
+  obtain hx' | hx' := lt_or_le x 0,
+  { exact (geom_sum_pos_and_lt_one hx' hx n.one_lt_succ_succ).1 },
+  { exact geom_sum_pos hx' (by simp only [nat.succ_ne_zero, ne.def, not_false_iff]) }
+end
+
 lemma odd.geom_sum_pos [linear_ordered_ring α] (h : odd n) :
   0 < ∑ i in range n, x ^ i :=
 begin
@@ -455,55 +482,47 @@ begin
     simp only [h, if_false] at this,
     exact zero_lt_one.trans this },
   { simp only [eq_neg_of_add_eq_zero_left hx, h, neg_one_geom_sum, if_false, zero_lt_one] },
-  rcases lt_trichotomy x 0 with hx' | rfl | hx',
-  { exact (geom_sum_pos_and_lt_one hx' hx k.one_lt_succ_succ).1 },
-  { simp only [zero_geom_sum, nat.succ_ne_zero, if_false, zero_lt_one] },
-  { exact geom_sum_pos hx' (by simp only [nat.succ_ne_zero, ne.def, not_false_iff]) }
+  { exact geom_sum_pos' hx k.succ.succ_ne_zero }
 end
 
-lemma geom_sum_pos_iff [linear_ordered_ring α] (hn : 1 < n) :
+lemma geom_sum_pos_iff [linear_ordered_ring α] (hn : n ≠ 0) :
   0 < ∑ i in range n, x ^ i ↔ odd n ∨ 0 < x + 1 :=
 begin
   refine ⟨λ h, _, _⟩,
-  { suffices : ¬ 0 < x + 1 → odd n, by tauto,
-    intro hx,
-    rw not_lt at hx,
-    contrapose! h,
-    rw [←nat.even_iff_not_odd] at h,
-    rcases hx.eq_or_lt with hx | hx,
-    { rw [←neg_neg (1 : α), add_neg_eq_iff_eq_add, zero_add] at hx,
-      simp only [hx, neg_one_geom_sum, h, if_true] },
-    apply le_of_lt,
-    simpa [h] using geom_sum_alternating_of_lt_neg_one hx hn },
+  { rw [or_iff_not_imp_left, ←not_le, ←nat.even_iff_not_odd],
+    refine λ hn hx, h.not_le _,
+    simpa [if_pos hn] using geom_sum_alternating_of_le_neg_one hx n },
   { rintro (hn | hx'),
     { exact hn.geom_sum_pos },
-    rcases lt_trichotomy x 0 with hx | rfl | hx,
-    { exact (geom_sum_pos_and_lt_one hx hx' hn).1 },
-    { simp only [(zero_lt_one.trans hn).ne', zero_geom_sum, if_false, zero_lt_one] },
-    { exact geom_sum_pos hx (zero_lt_one.trans hn).ne' } }
+    { exact geom_sum_pos' hx' hn } }
 end
 
-lemma geom_sum_eq_zero_iff_neg_one [linear_ordered_ring α] (hn : 1 < n) :
+lemma geom_sum_ne_zero [linear_ordered_ring α] (hx : x ≠ -1) (hn : n ≠ 0) :
+  ∑ i in range n, x ^ i ≠ 0 :=
+begin
+  obtain _ | _ | n := n,
+  { cases hn rfl },
+  { simp },
+  rw [ne.def, eq_neg_iff_add_eq_zero, ←ne.def] at hx,
+  obtain h | h := hx.lt_or_lt,
+  { have := geom_sum_alternating_of_lt_neg_one h n.one_lt_succ_succ,
+    split_ifs at this,
+    { exact this.ne },
+    { exact (zero_lt_one.trans this).ne' } },
+  { exact (geom_sum_pos' h n.succ.succ_ne_zero).ne' }
+end
+
+lemma geom_sum_eq_zero_iff_neg_one [linear_ordered_ring α] (hn : n ≠ 0) :
   ∑ i in range n, x ^ i = 0 ↔ x = -1 ∧ even n :=
 begin
   refine ⟨λ h, _, λ ⟨h, hn⟩, by simp only [h, hn, neg_one_geom_sum, if_true]⟩,
   contrapose! h,
-  rcases eq_or_ne x (-1) with rfl | h,
+  obtain rfl | hx := eq_or_ne x (-1),
   { simp only [h rfl, neg_one_geom_sum, if_false, ne.def, not_false_iff, one_ne_zero] },
-  rw [ne.def, eq_neg_iff_add_eq_zero, ←ne.def] at h,
-  rcases h.lt_or_lt with h | h,
-  { have := geom_sum_alternating_of_lt_neg_one h hn,
-    split_ifs at this,
-    { exact this.ne },
-    { exact (zero_lt_one.trans this).ne' } },
-  apply ne_of_gt,
-  rcases lt_trichotomy x 0 with h' | rfl | h',
-  { exact (geom_sum_pos_and_lt_one h' h hn).1 },
-  { simp only [(pos_of_gt hn).ne', zero_geom_sum, if_false, zero_lt_one] },
-  { exact geom_sum_pos h' (pos_of_gt hn).ne' }
+  { exact geom_sum_ne_zero hx hn }
 end
 
-lemma geom_sum_neg_iff [linear_ordered_ring α] (hn : 1 < n) :
+lemma geom_sum_neg_iff [linear_ordered_ring α] (hn : n ≠ 0) :
   ∑ i in range n, x ^ i < 0 ↔ even n ∧ x + 1 < 0 :=
 by rw [← not_iff_not, not_lt, le_iff_lt_or_eq, eq_comm,
        or_congr (geom_sum_pos_iff hn) (geom_sum_eq_zero_iff_neg_one hn), nat.odd_iff_not_even,

src/algebra/group_power/lemmas.lean

@@ -423,8 +423,8 @@ end
 lemma neg_one_pow_eq_pow_mod_two [ring R] {n : ℕ} : (-1 : R) ^ n = (-1) ^ (n % 2) :=
 by rw [← nat.mod_add_div n 2, pow_add, pow_mul]; simp [sq]
 
-section ordered_semiring
-variables [ordered_semiring R] {a : R}
+section strict_ordered_semiring
+variables [strict_ordered_semiring R] {a : R}
 
 /-- Bernoulli's inequality. This version works for semirings but requires
 additional hypotheses `0 ≤ a * a` and `0 ≤ (1 + a) * (1 + a)`. -/
@@ -461,7 +461,7 @@ lemma pow_le_of_le_one (h₀ : 0 ≤ a) (h₁ : a ≤ 1) {n : ℕ} (hn : n ≠ 0
 
 lemma sq_le (h₀ : 0 ≤ a) (h₁ : a ≤ 1) : a ^ 2 ≤ a := pow_le_of_le_one h₀ h₁ two_ne_zero
 
-end ordered_semiring
+end strict_ordered_semiring
 
 section linear_ordered_semiring
 

src/algebra/group_power/order.lean

@@ -222,6 +222,15 @@ begin
       by { rw [pow_succ _ n], exact mul_le_mul_of_nonneg_left (ih (nat.succ_ne_zero k)) h2 }
 end
 
+lemma pow_le_one : ∀ (n : ℕ) (h₀ : 0 ≤ a) (h₁ : a ≤ 1), a ^ n ≤ 1
+| 0       h₀ h₁ := (pow_zero a).le
+| (n + 1) h₀ h₁ := (pow_succ' a n).le.trans (mul_le_one (pow_le_one n h₀ h₁) h₀ h₁)
+
+lemma pow_lt_one (h₀ : 0 ≤ a) (h₁ : a < 1) : ∀ {n : ℕ} (hn : n ≠ 0), a ^ n < 1
+| 0 h := (h rfl).elim
+| (n + 1) h :=
+  by { rw pow_succ, exact mul_lt_one_of_nonneg_of_lt_one_left h₀ h₁ (pow_le_one _ h₀ h₁.le) }
+
 theorem one_le_pow_of_one_le (H : 1 ≤ a) : ∀ (n : ℕ), 1 ≤ a ^ n
 | 0     := by rw [pow_zero]
 | (n+1) := by { rw pow_succ, simpa only [mul_one] using mul_le_mul H (one_le_pow_of_one_le n)
@@ -237,6 +246,29 @@ pow_mono ha h
 theorem le_self_pow (ha : 1 ≤ a) (h : m ≠ 0) : a ≤ a ^ m :=
 (pow_one a).symm.trans_le (pow_le_pow ha $ pos_iff_ne_zero.mpr h)
 
+@[mono] lemma pow_le_pow_of_le_left {a b : R} (ha : 0 ≤ a) (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 _) (pow_nonneg ha _) (le_trans ha hab) }
+
+lemma one_lt_pow (ha : 1 < a) : ∀ {n : ℕ} (hn : n ≠ 0), 1 < a ^ n
+| 0 h := (h rfl).elim
+| (n + 1) h :=
+  by { rw pow_succ, exact one_lt_mul_of_lt_of_le ha (one_le_pow_of_one_le ha.le _) }
+
+end ordered_semiring
+
+section strict_ordered_semiring
+variables [strict_ordered_semiring R] {a x y : R} {n m : ℕ}
+
+lemma pow_lt_pow_of_lt_left (h : x < y) (hx : 0 ≤ x) : ∀ {n : ℕ}, 0 < n → x ^ n < y ^ n
+| 0 hn := hn.false.elim
+| (n + 1) _ := by simpa only [pow_succ'] using
+    mul_lt_mul_of_le_of_le' (pow_le_pow_of_le_left hx h.le _) h (pow_pos (hx.trans_lt h) _) hx
+
+lemma strict_mono_on_pow (hn : 0 < n) : strict_mono_on (λ x : R, x ^ n) (set.Ici 0) :=
+λ x hx y hy h, pow_lt_pow_of_lt_left h hx hn
+
 lemma strict_mono_pow (h : 1 < a) : strict_mono (λ n : ℕ, a ^ n) :=
 have 0 < a := zero_le_one.trans_lt h,
 strict_mono_nat_of_lt_succ $ λ n, by simpa only [one_mul, pow_succ]
@@ -261,37 +293,12 @@ lemma pow_lt_pow_iff_of_lt_one (h₀ : 0 < a) (h₁ : a < 1) : a ^ m < a ^ n ↔
 lemma pow_lt_pow_of_lt_one (h : 0 < a) (ha : a < 1) {i j : ℕ} (hij : i < j) : a ^ j < a ^ i :=
 (pow_lt_pow_iff_of_lt_one h ha).2 hij
 
-@[mono] lemma pow_le_pow_of_le_left {a b : R} (ha : 0 ≤ a) (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 _) (pow_nonneg ha _) (le_trans ha hab) }
-
-lemma pow_lt_pow_of_lt_left (h : x < y) (hx : 0 ≤ x) : ∀ {n : ℕ}, 0 < n → x ^ n < y ^ n
-| 0 hn := hn.false.elim
-| (n + 1) _ := by simpa only [pow_succ'] using
-    mul_lt_mul' (pow_le_pow_of_le_left hx h.le _) h hx (pow_pos (hx.trans_lt h) _)
-
-lemma pow_lt_one (h₀ : 0 ≤ a) (h₁ : a < 1) {n : ℕ} (hn : n ≠ 0) : a ^ n < 1 :=
-(one_pow n).subst (pow_lt_pow_of_lt_left h₁ h₀ (nat.pos_of_ne_zero hn))
-
-lemma one_lt_pow (ha : 1 < a) {n : ℕ} (hn : n ≠ 0) : 1 < a ^ n :=
-pow_zero a ▸ pow_lt_pow ha (pos_iff_ne_zero.2 hn)
-
-lemma pow_le_one : ∀ (n : ℕ) (h₀ : 0 ≤ a) (h₁ : a ≤ 1), a ^ n ≤ 1
-| 0       h₀ h₁ := (pow_zero a).le
-| (n + 1) h₀ h₁ := (pow_succ' a n).le.trans (mul_le_one (pow_le_one n h₀ h₁) h₀ h₁)
-
-lemma strict_mono_on_pow (hn : 0 < n) : strict_mono_on (λ x : R, x ^ n) (set.Ici 0) :=
-λ x hx y hy h, pow_lt_pow_of_lt_left h hx hn
-
 lemma sq_pos_of_pos (ha : 0 < a) : 0 < a ^ 2 := by { rw sq, exact mul_pos ha ha }
 
-end ordered_semiring
+end strict_ordered_semiring
 
-section ordered_ring
-variables [ordered_ring R] {a : R}
-
-lemma sq_pos_of_neg (ha : a < 0) : 0 < a ^ 2 := by { rw sq, exact mul_pos_of_neg_of_neg ha ha }
+section strict_ordered_ring
+variables [strict_ordered_ring R] {a : R}
 
 lemma pow_bit0_pos_of_neg (ha : a < 0) (n : ℕ) : 0 < a ^ bit0 n :=
 begin
@@ -305,7 +312,9 @@ begin
   exact mul_neg_of_neg_of_pos ha (pow_bit0_pos_of_neg ha n),
 end
 
-end ordered_ring
+lemma sq_pos_of_neg (ha : a < 0) : 0 < a ^ 2 := pow_bit0_pos_of_neg ha _
+
+end strict_ordered_ring
 
 section linear_ordered_semiring
 variables [linear_ordered_semiring R] {a b : R}

src/algebra/ne_zero.lean

@@ -62,7 +62,7 @@ instance bit0 [canonically_ordered_add_monoid M] [ne_zero x] : ne_zero (bit0 x)
 of_pos $ bit0_pos $ ne_zero.pos x
 
 instance bit1 [canonically_ordered_comm_semiring M] [nontrivial M] : ne_zero (bit1 x) :=
-⟨mt (λ h, le_iff_exists_add'.2 ⟨_, h.symm⟩) canonically_ordered_comm_semiring.zero_lt_one.not_le⟩
+⟨mt (λ h, le_iff_exists_add'.2 ⟨_, h.symm⟩) zero_lt_one.not_le⟩
 
 instance pow [monoid_with_zero M] [no_zero_divisors M] [ne_zero x] : ne_zero (x ^ n) :=
 ⟨pow_ne_zero n out⟩

src/algebra/order/algebra.lean

@@ -45,13 +45,3 @@ begin
 end
 
 end ordered_algebra
-
-section instances
-
-variables {R : Type*} [linear_ordered_comm_ring R]
-
-instance linear_ordered_comm_ring.to_ordered_smul : ordered_smul R R :=
-{ smul_lt_smul_of_pos       := ordered_semiring.mul_lt_mul_of_pos_left,
-  lt_of_smul_lt_smul_of_pos := λ a b c w₁ w₂, (mul_lt_mul_left w₂).mp w₁ }
-
-end instances