feat(algebra/ordered*): more simp lemmas (#4359)

Simplify expressions like `0 < a * b`, `0 < a / b`, `a / b < 1` etc. to FOL formulas of inequalities on `a`, `b`.

Author: urkud

src/algebra/gcd_monoid.lean

@@ -461,11 +461,8 @@ instance : normalization_monoid ℤ :=
   norm_unit_zero := if_pos (le_refl _),
   norm_unit_mul  := assume a b hna hnb,
   begin
-    by_cases ha : 0 ≤ a; by_cases hb : 0 ≤ b; simp [ha, hb],
-    exact if_pos (mul_nonneg ha hb),
-    exact if_neg (assume h, hb $ nonneg_of_mul_nonneg_left h $ lt_of_le_of_ne ha hna.symm),
-    exact if_neg (assume h, ha $ nonneg_of_mul_nonneg_right h $ lt_of_le_of_ne hb hnb.symm),
-    exact if_pos (mul_nonneg_of_nonpos_of_nonpos (le_of_not_ge ha) (le_of_not_ge hb))
+    cases hna.lt_or_lt with ha ha; cases hnb.lt_or_lt with hb hb;
+      simp [mul_nonneg_iff, ha.le, ha.not_le, hb.le, hb.not_le]
   end,
   norm_unit_coe_units := assume u, (units_eq_one_or u).elim
     (assume eq, eq.symm ▸ if_pos zero_le_one)

src/algebra/group_power/basic.lean

@@ -485,11 +485,11 @@ end canonically_ordered_semiring
 section linear_ordered_semiring
 variable [linear_ordered_semiring R]
 
-theorem pow_pos {a : R} (H : 0 < a) : ∀ (n : ℕ), 0 < a ^ n
+@[simp] theorem pow_pos {a : R} (H : 0 < a) : ∀ (n : ℕ), 0 < a ^ n
 | 0     := zero_lt_one
 | (n+1) := mul_pos H (pow_pos _)
 
-theorem pow_nonneg {a : R} (H : 0 ≤ a) : ∀ (n : ℕ), 0 ≤ a ^ n
+@[simp] theorem pow_nonneg {a : R} (H : 0 ≤ a) : ∀ (n : ℕ), 0 ≤ a ^ n
 | 0     := zero_le_one
 | (n+1) := mul_nonneg H (pow_nonneg _)
 

src/algebra/group_with_zero.lean

@@ -510,6 +510,9 @@ inv_involutive'.injective
 lemma inv_eq_iff {g h : G₀} : g⁻¹ = h ↔ h⁻¹ = g :=
 by rw [← inv_inj', eq_comm, inv_inv']
 
+@[simp] lemma inv_eq_one' {g : G₀} : g⁻¹ = 1 ↔ g = 1 :=
+by rw [inv_eq_iff, inv_one, eq_comm]
+
 end group_with_zero
 
 namespace units

src/algebra/order.lean

@@ -111,6 +111,9 @@ h.lt_or_eq.symm
 
 alias eq_or_lt_of_le ← has_le.le.eq_or_lt
 
+lemma ne.le_iff_lt [partial_order α] {a b : α} (h : a ≠ b) : a ≤ b ↔ a < b :=
+⟨λ h', lt_of_le_of_ne h' h, λ h, h.le⟩
+
 lemma lt_of_not_ge' [linear_order α] {a b : α} (h : ¬ b ≤ a) : a < b :=
 ((le_total _ _).resolve_right h).lt_of_not_le h
 
@@ -122,6 +125,9 @@ lemma le_of_not_lt [linear_order α] {a b : α} : ¬ a < b → b ≤ a := not_lt
 lemma lt_or_le [linear_order α] : ∀ a b : α, a < b ∨ b ≤ a := lt_or_ge
 lemma le_or_lt [linear_order α] : ∀ a b : α, a ≤ b ∨ b < a := le_or_gt
 
+lemma ne.lt_or_lt [linear_order α] {a b : α} (h : a ≠ b) : a < b ∨ b < a :=
+lt_or_gt_of_ne h
+
 lemma has_le.le.lt_or_le [linear_order α] {a b : α} (h : a ≤ b) (c : α) : a < c ∨ c ≤ b :=
 (lt_or_le a c).imp id $ λ hc, hc.trans h
 

src/algebra/ordered_field.lean

@@ -58,6 +58,18 @@ inv_eq_one_div a ▸ inv_nonneg
 lemma one_div_nonpos : 1 / a ≤ 0 ↔ a ≤ 0 :=
 inv_eq_one_div a ▸ inv_nonpos
 
+lemma div_pos_iff : 0 < a / b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0 :=
+by simp [division_def, mul_pos_iff]
+
+lemma div_neg_iff : a / b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b :=
+by simp [division_def, mul_neg_iff]
+
+lemma div_nonneg_iff : 0 ≤ a / b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 :=
+by simp [division_def, mul_nonneg_iff]
+
+lemma div_nonpos_iff : a / b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b :=
+by simp [division_def, mul_nonpos_iff]
+
 lemma div_pos (ha : 0 < a) (hb : 0 < b) : 0 < a / b :=
 mul_pos ha (inv_pos.2 hb)
 
@@ -240,6 +252,29 @@ by rwa [inv_le ((@zero_lt_one α _).trans_le ha) zero_lt_one, inv_one]
 lemma one_le_inv (h₁ : 0 < a) (h₂ : a ≤ 1) : 1 ≤ a⁻¹ :=
 by rwa [le_inv (@zero_lt_one α _) h₁, inv_one]
 
+lemma inv_lt_one_iff_of_pos (h₀ : 0 < a) : a⁻¹ < 1 ↔ 1 < a :=
+⟨λ h₁, inv_inv' a ▸ one_lt_inv (inv_pos.2 h₀) h₁, inv_lt_one⟩
+
+lemma inv_lt_one_iff : a⁻¹ < 1 ↔ a ≤ 0 ∨ 1 < a :=
+begin
+  cases le_or_lt a 0 with ha ha,
+  { simp [ha, (inv_nonpos.2 ha).trans_lt zero_lt_one] },
+  { simp only [ha.not_le, false_or, inv_lt_one_iff_of_pos ha] }
+end
+
+lemma one_lt_inv_iff : 1 < a⁻¹ ↔ 0 < a ∧ a < 1 :=
+⟨λ h, ⟨inv_pos.1 (zero_lt_one.trans h), inv_inv' a ▸ inv_lt_one h⟩, and_imp.2 one_lt_inv⟩
+
+lemma inv_le_one_iff : a⁻¹ ≤ 1 ↔ a ≤ 0 ∨ 1 ≤ a :=
+begin
+  rcases em (a = 1) with (rfl|ha),
+  { simp [le_rfl] },
+  { simp only [ne.le_iff_lt (ne.symm ha), ne.le_iff_lt (mt inv_eq_one'.1 ha), inv_lt_one_iff] }
+end
+
+lemma one_le_inv_iff : 1 ≤ a⁻¹ ↔ 0 < a ∧ a ≤ 1 :=
+⟨λ h, ⟨inv_pos.1 (zero_lt_one.trans_le h), inv_inv' a ▸ inv_le_one h⟩, and_imp.2 one_le_inv⟩
+
 /-!
 ### Relating two divisions.
 -/
@@ -368,6 +403,38 @@ by simpa using le_inv_of_neg ha hb
 lemma lt_one_div_of_neg (ha : a < 0) (hb : b < 0) : a < 1 / b ↔ b < 1 / a :=
 by simpa using lt_inv_of_neg ha hb
 
+lemma one_lt_div_iff : 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b :=
+begin
+  rcases lt_trichotomy b 0 with (hb|rfl|hb),
+  { simp [hb, hb.not_lt, one_lt_div_of_neg] },
+  { simp [lt_irrefl, zero_le_one] },
+  { simp [hb, hb.not_lt, one_lt_div] }
+end
+
+lemma one_le_div_iff : 1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b :=
+begin
+  rcases lt_trichotomy b 0 with (hb|rfl|hb),
+  { simp [hb, hb.not_lt, one_le_div_of_neg] },
+  { simp [lt_irrefl, zero_lt_one.not_le, zero_lt_one] },
+  { simp [hb, hb.not_lt, one_le_div] }
+end
+
+lemma div_lt_one_iff : a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a :=
+begin
+  rcases lt_trichotomy b 0 with (hb|rfl|hb),
+  { simp [hb, hb.not_lt, hb.ne, div_lt_one_of_neg] },
+  { simp [zero_lt_one], },
+  { simp [hb, hb.not_lt, div_lt_one, hb.ne.symm] }
+end
+
+lemma div_le_one_iff : a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a :=
+begin
+  rcases lt_trichotomy b 0 with (hb|rfl|hb),
+  { simp [hb, hb.not_lt, hb.ne, div_le_one_of_neg] },
+  { simp [zero_le_one], },
+  { simp [hb, hb.not_lt, div_le_one, hb.ne.symm] }
+end
+
 /-!
 ### Relating two divisions, involving `1`
 -/

src/algebra/ordered_ring.lean

@@ -197,17 +197,33 @@ le_of_not_gt
    have h2 : b * c < a * c, from mul_lt_mul_of_pos_right h1 hc,
    h2.not_le h)
 
-lemma pos_of_mul_pos_left (h : 0 < a * b) (h1 : 0 ≤ a) : 0 < b :=
-lt_of_not_ge
-  (assume h2 : b ≤ 0,
-   have h3 : a * b ≤ 0, from mul_nonpos_of_nonneg_of_nonpos h1 h2,
-   h3.not_lt h)
+lemma pos_and_pos_or_neg_and_neg_of_mul_pos (hab : 0 < a * b) :
+    (0 < a ∧ 0 < b) ∨ (a < 0 ∧ b < 0) :=
+begin
+  rcases lt_trichotomy 0 a with (ha|rfl|ha),
+  { refine or.inl ⟨ha, _⟩,
+    contrapose! hab,
+    exact mul_nonpos_of_nonneg_of_nonpos ha.le hab },
+  { rw [zero_mul] at hab, exact hab.false.elim },
+  { refine or.inr ⟨ha, _⟩,
+    contrapose! hab,
+    exact mul_nonpos_of_nonpos_of_nonneg ha.le hab }
+end
 
-lemma pos_of_mul_pos_right (h : 0 < a * b) (h1 : 0 ≤ b) : 0 < a :=
-lt_of_not_ge
-  (assume h2 : a ≤ 0,
-   have h3 : a * b ≤ 0, from mul_nonpos_of_nonpos_of_nonneg h2 h1,
-   h3.not_lt h)
+lemma nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nnonneg (hab : 0 ≤ a * b) :
+    (0 ≤ a ∧ 0 ≤ b) ∨ (a ≤ 0 ∧ b ≤ 0) :=
+begin
+  contrapose! hab,
+  rcases lt_trichotomy 0 a with (ha|rfl|ha),
+  exacts [mul_neg_of_pos_of_neg ha (hab.1 ha.le), ((hab.1 le_rfl).asymm (hab.2 le_rfl)).elim,
+    mul_neg_of_neg_of_pos ha (hab.2 ha.le)]
+end
+
+lemma pos_of_mul_pos_left (h : 0 < a * b) (ha : 0 ≤ a) : 0 < b :=
+((pos_and_pos_or_neg_and_neg_of_mul_pos h).resolve_right $ λ h, h.1.not_le ha).2
+
+lemma pos_of_mul_pos_right (h : 0 < a * b) (hb : 0 ≤ b) : 0 < a :=
+((pos_and_pos_or_neg_and_neg_of_mul_pos h).resolve_right $ λ h, h.2.not_le hb).1
 
 lemma nonneg_of_mul_nonneg_left (h : 0 ≤ a * b) (h1 : 0 < a) : 0 ≤ b :=
 le_of_not_gt (assume h2 : b < 0, (mul_neg_of_pos_of_neg h1 h2).not_le h)
@@ -523,29 +539,37 @@ instance linear_ordered_ring.to_linear_ordered_semiring : linear_ordered_semirin
   le_total                   := linear_ordered_ring.le_total,
   ..‹linear_ordered_ring α› }
 
+@[priority 100] -- see Note [lower instance priority]
+instance linear_ordered_ring.to_domain : domain α :=
+{ eq_zero_or_eq_zero_of_mul_eq_zero :=
+    begin
+      intros a b hab,
+      contrapose! hab,
+      cases (lt_or_gt_of_ne hab.1) with ha ha; cases (lt_or_gt_of_ne hab.2) with hb hb,
+      exacts [(mul_pos_of_neg_of_neg ha hb).ne.symm, (mul_neg_of_neg_of_pos ha hb).ne,
+        (mul_neg_of_pos_of_neg ha hb).ne, (mul_pos ha hb).ne.symm]
+    end,
+  .. ‹linear_ordered_ring α› }
+
+lemma mul_pos_iff : 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0 :=
+⟨pos_and_pos_or_neg_and_neg_of_mul_pos,
+  λ h, h.elim (and_imp.2 mul_pos) (and_imp.2 mul_pos_of_neg_of_neg)⟩
+
+lemma mul_neg_iff : a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b :=
+by rw [← neg_pos, neg_mul_eq_mul_neg, mul_pos_iff, neg_pos, neg_lt_zero]
+
+lemma mul_nonneg_iff : 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 :=
+⟨nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nnonneg,
+  λ h, h.elim (and_imp.2 mul_nonneg) (and_imp.2 mul_nonneg_of_nonpos_of_nonpos)⟩
+
+lemma mul_nonpos_iff : a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b :=
+by rw [← neg_nonneg, neg_mul_eq_mul_neg, mul_nonneg_iff, neg_nonneg, neg_nonpos]
+
 lemma mul_self_nonneg (a : α) : 0 ≤ a * a :=
 or.elim (le_total 0 a)
   (assume h : a ≥ 0, mul_nonneg h h)
   (assume h : a ≤ 0, mul_nonneg_of_nonpos_of_nonpos h h)
 
-lemma pos_and_pos_or_neg_and_neg_of_mul_pos (hab : 0 < a * b) :
-    (0 < a ∧ 0 < b) ∨ (a < 0 ∧ b < 0) :=
-match lt_trichotomy 0 a with
-| or.inl hlt₁          :=
-  match lt_trichotomy 0 b with
-  | or.inl hlt₂          := or.inl ⟨hlt₁, hlt₂⟩
-  | or.inr (or.inl heq₂) := begin rw [← heq₂, mul_zero] at hab, exact absurd hab (lt_irrefl _) end
-  | or.inr (or.inr hgt₂) := absurd hab (lt_asymm (mul_neg_of_pos_of_neg hlt₁ hgt₂))
-  end
-| or.inr (or.inl heq₁) := begin rw [← heq₁, zero_mul] at hab, exact absurd hab (lt_irrefl _) end
-| or.inr (or.inr hgt₁) :=
-  match lt_trichotomy 0 b with
-  | or.inl hlt₂          := absurd hab (lt_asymm (mul_neg_of_neg_of_pos hgt₁ hlt₂))
-  | or.inr (or.inl heq₂) := begin rw [← heq₂, mul_zero] at hab, exact absurd hab (lt_irrefl _) end
-  | or.inr (or.inr hgt₂) := or.inr ⟨hgt₁, hgt₂⟩
-  end
-end
-
 lemma gt_of_mul_lt_mul_neg_left (h : c * a < c * b) (hc : c ≤ 0) : b < a :=
 have nhc : 0 ≤ -c, from neg_nonneg_of_nonpos hc,
 have h2 : -(c * b) < -(c * a), from neg_lt_neg h,
@@ -555,7 +579,6 @@ have h3 : (-c) * b < (-c) * a, from calc
           ... = (-c) * a     : by rewrite neg_mul_eq_neg_mul,
 lt_of_mul_lt_mul_left h3 nhc
 
-
 lemma neg_one_lt_zero : -1 < (0:α) :=
 begin
   have this := neg_lt_neg (@zero_lt_one α _),
@@ -579,44 +602,13 @@ lemma mul_self_lt_mul_self_iff {a b : α} (h1 : 0 ≤ a) (h2 : 0 ≤ b) : a < b
 iff.trans (lt_iff_not_ge _ _) $ iff.trans (not_iff_not_of_iff $ mul_self_le_mul_self_iff h2 h1) $
   iff.symm (lt_iff_not_ge _ _)
 
-lemma linear_ordered_ring.eq_zero_or_eq_zero_of_mul_eq_zero
-  {a b : α} (h : a * b = 0) : a = 0 ∨ b = 0 :=
-match lt_trichotomy 0 a with
-| or.inl hlt₁          :=
-  match lt_trichotomy 0 b with
-  | or.inl hlt₂          :=
-    have 0 < a * b, from mul_pos hlt₁ hlt₂,
-    begin rw h at this, exact absurd this (lt_irrefl _) end
-  | or.inr (or.inl heq₂) := or.inr heq₂.symm
-  | or.inr (or.inr hgt₂) :=
-    have 0 > a * b, from mul_neg_of_pos_of_neg hlt₁ hgt₂,
-    begin rw h at this, exact absurd this (lt_irrefl _)  end
-  end
-| or.inr (or.inl heq₁) := or.inl heq₁.symm
-| or.inr (or.inr hgt₁) :=
-  match lt_trichotomy 0 b with
-  | or.inl hlt₂          :=
-    have 0 > a * b, from mul_neg_of_neg_of_pos hgt₁ hlt₂,
-    begin rw h at this, exact absurd this (lt_irrefl _)  end
-  | or.inr (or.inl heq₂) := or.inr heq₂.symm
-  | or.inr (or.inr hgt₂) :=
-    have 0 < a * b, from mul_pos_of_neg_of_neg hgt₁ hgt₂,
-    begin rw h at this, exact absurd this (lt_irrefl _)  end
-  end
-end
-
 /- TODO This theorem ought to be written in the context of `nontrivial` linearly ordered (additive)
 commutative groups rather than linearly ordered rings; however, the former concept does not
 currently exist in mathlib. -/
 @[priority 100] -- see Note [lower instance priority]
 instance linear_ordered_ring.to_no_bot_order : no_bot_order α :=
 ⟨assume a, ⟨a - 1, sub_lt_iff_lt_add.mpr $ lt_add_of_pos_right _ zero_lt_one⟩⟩
 
-@[priority 100] -- see Note [lower instance priority]
-instance linear_ordered_ring.to_domain : domain α :=
-{ eq_zero_or_eq_zero_of_mul_eq_zero := @linear_ordered_ring.eq_zero_or_eq_zero_of_mul_eq_zero α _,
-  ..‹linear_ordered_ring α› }
-
 @[simp] lemma mul_le_mul_left_of_neg {a b c : α} (h : c < 0) : c * a ≤ c * b ↔ b ≤ a :=
 ⟨le_imp_le_of_lt_imp_lt $ λ h', mul_lt_mul_of_neg_left h' h,
   λ h', mul_le_mul_of_nonpos_left h' h.le⟩
@@ -675,9 +667,9 @@ such that multiplication with a positive number and addition are monotone. -/
 class linear_ordered_comm_ring (α : Type u) extends linear_ordered_ring α, comm_monoid α
 
 @[priority 100] -- see Note [lower instance priority]
-instance linear_ordered_comm_ring.to_integral_domain [s: linear_ordered_comm_ring α] : integral_domain α :=
-{ eq_zero_or_eq_zero_of_mul_eq_zero := @linear_ordered_ring.eq_zero_or_eq_zero_of_mul_eq_zero α _,
-  ..s }
+instance linear_ordered_comm_ring.to_integral_domain [s: linear_ordered_comm_ring α] :
+  integral_domain α :=
+{ ..s, .. linear_ordered_ring.to_domain }
 
 /-- A `decidable_linear_ordered_comm_ring α` is a commutative ring `α` with a
 decidable linear order such that multiplication with a positive number and
@@ -786,17 +778,14 @@ begin
   apply sub_le_sub_left,
   iterate {rw mul_assoc},
   apply mul_le_mul_of_nonneg_left,
-  rw [← abs_mul],
-  apply le_abs_self,
-  apply le_of_lt,
-  apply add_pos,
-  apply zero_lt_one,
-  apply zero_lt_one
+  { rw [← abs_mul],
+    apply le_abs_self },
+  { exact (add_pos (@zero_lt_one α _) zero_lt_one).le }
 end
 
 -- The proof doesn't need commutativity but we have no `decidable_linear_ordered_ring`
 @[simp] lemma abs_two : abs (2:α) = 2 :=
-abs_of_pos $ by refine zero_lt_two
+abs_of_pos zero_lt_two
 
 end decidable_linear_ordered_comm_ring
 

src/analysis/hofer.lean

@@ -48,6 +48,7 @@ begin
   choose! F hF using H,  -- Use the axiom of choice
   -- Now define u by induction starting at x, with u_{n+1} = F(n, u_n)
   let u : ℕ → X := λ n, nat.rec_on n x F,
+  have hu0 : u 0 = x := rfl,
   -- The properties of F translate to properties of u
   have hu :
     ∀ n,
@@ -56,14 +57,12 @@ begin
   { intro n,
     exact hF n (u n) },
   clear hF,
-
   -- Key properties of u, to be proven by induction
   have key : ∀ n, d (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ 2 * ϕ (u n) < ϕ (u (n + 1)),
   { intro n,
     induction n using nat.case_strong_induction_on with n IH,
     { specialize hu 0,
-      simp [show u 0 = x, from rfl, le_refl] at *,
-      exact hu (by linarith) },
+      simpa [hu0, mul_nonneg_iff, zero_le_one, ε_pos.le] using hu },
     have A : d (u (n+1)) x ≤ 2 * ε,
     { rw [dist_comm],
       let r := range (n+1), -- range (n+1) = {0, ..., n}
@@ -82,18 +81,15 @@ begin
     exact hu (n+1) ⟨A, B⟩, },
   cases forall_and_distrib.mp key with key₁ key₂,
   clear hu key,
-
   -- Hence u is Cauchy
   have cauchy_u : cauchy_seq u,
   { apply cauchy_seq_of_le_geometric _ ε (by norm_num : 1/(2:ℝ) < 1),
     intro n,
     convert key₁ n,
     simp },
-
   -- So u converges to some y
   obtain ⟨y, limy⟩ : ∃ y, tendsto u at_top (𝓝 y),
     from complete_space.complete cauchy_u,
-
   -- And ϕ ∘ u goes to +∞
   have lim_top : tendsto (ϕ ∘ u) at_top at_top,
   { let v := λ n, (ϕ ∘ u) (n+1),
@@ -105,11 +101,9 @@ begin
       ... < ϕ (u (0 + 1)) : key₂ 0 },
     apply tendsto_at_top_of_geom_lt hv₀ (by norm_num : (1 : ℝ) < 2),
     exact λ n, key₂ (n+1) },
-
   -- But ϕ ∘ u also needs to go to ϕ(y)
   have lim : tendsto (ϕ ∘ u) at_top (𝓝 (ϕ y)),
     from tendsto.comp cont.continuous_at limy,
-
   -- So we have our contradiction!
   exact not_tendsto_at_top_of_tendsto_nhds lim lim_top,
 end

src/data/int/basic.lean

@@ -100,7 +100,7 @@ by rw [← int.coe_nat_zero, coe_nat_inj']
 theorem coe_nat_ne_zero {n : ℕ} : (n : ℤ) ≠ 0 ↔ n ≠ 0 :=
 not_congr coe_nat_eq_zero
 
-lemma coe_nat_nonneg (n : ℕ) : 0 ≤ (n : ℤ) := coe_nat_le.2 (nat.zero_le _)
+@[simp] lemma coe_nat_nonneg (n : ℕ) : 0 ≤ (n : ℤ) := coe_nat_le.2 (nat.zero_le _)
 
 lemma coe_nat_ne_zero_iff_pos {n : ℕ} : (n : ℤ) ≠ 0 ↔ 0 < n :=
 ⟨λ h, nat.pos_of_ne_zero (coe_nat_ne_zero.1 h),