feat(algebra/divisibility/basic): Dot notation aliases (#18698)

A few convenience shortcuts for `dvd` along with some simple `nat` lemmas. Also
* Drop `neg_dvd_of_dvd`/`dvd_of_neg_dvd`/`dvd_neg_of_dvd`/`dvd_of_dvd_neg` in favor of the aforementioned shortcuts.
* Remove explicit arguments to `dvd_neg`/`neg_dvd`.
* Drop `int.of_nat_dvd_of_dvd_nat_abs`/`int.dvd_nat_abs_of_of_nat_dvd` because they are the two directions of `int.coe_nat_dvd_left`.
* Move `group_with_zero.to_cancel_monoid_with_zero` from `algebra.group_with_zero.units.basic` back to `algebra.group_with_zero.basic`. It was erroneously moved during the Great Splits.

archive/imo/imo1988_q6.lean

@@ -266,7 +266,7 @@ begin
     have x_sq_dvd : x*x ∣ x*x*k := dvd_mul_right (x*x) k,
     rw ← hx at x_sq_dvd,
     obtain ⟨y, hy⟩ : x * x ∣ 1 := by simpa only [nat.dvd_add_self_left, add_assoc] using x_sq_dvd,
-    obtain ⟨rfl,rfl⟩ : x = 1 ∧ y = 1 := by simpa [nat.mul_eq_one_iff] using hy.symm,
+    obtain ⟨rfl,rfl⟩ : x = 1 ∧ y = 1 := by simpa [mul_eq_one] using hy.symm,
     simpa using hx.symm, },
   { -- Show the descent step.
     intros x y x_lt_y hx h_base h z h_root hV₁ hV₀,

archive/imo/imo2011_q5.lean

@@ -47,7 +47,7 @@ begin
       { -- d = 0
         exact hd },
       { -- d < 0
-        have h₁ : f n ≤ -d, from le_of_dvd (neg_pos.mpr hd) ((dvd_neg _ _).mpr h_fn_dvd_d),
+        have h₁ : f n ≤ -d, from le_of_dvd (neg_pos.mpr hd) h_fn_dvd_d.neg_right,
         have h₂ : ¬ f n ≤ -d, from not_le.mpr h_neg_d_lt_fn,
         contradiction } },
     have h₁ : f m = f (m - n), from sub_eq_zero.mp h_d_eq_zero,

src/algebra/divisibility/basic.lean

@@ -91,14 +91,18 @@ end semigroup
 
 section monoid
 
-variables [monoid α]
+variables [monoid α] {a b : α}
 
 @[refl, simp] theorem dvd_refl (a : α) : a ∣ a := dvd.intro 1 (mul_one a)
 theorem dvd_rfl : ∀ {a : α}, a ∣ a := dvd_refl
 instance : is_refl α (∣) := ⟨dvd_refl⟩
 
 theorem one_dvd (a : α) : 1 ∣ a := dvd.intro a (one_mul a)
 
+lemma dvd_of_eq (h : a = b) : a ∣ b := by rw h
+
+alias dvd_of_eq ← eq.dvd
+
 end monoid
 
 section comm_semigroup

src/algebra/euclidean_domain/basic.lean

@@ -54,7 +54,7 @@ by { rw mul_comm, exact mul_div_cancel_left a b0 }
 mod_eq_zero.2 dvd_rfl
 
 lemma dvd_mod_iff {a b c : R} (h : c ∣ b) : c ∣ a % b ↔ c ∣ a :=
-by rw [dvd_add_iff_right (h.mul_right _), div_add_mod]
+by rw [←dvd_add_right (h.mul_right _), div_add_mod]
 
 @[simp] lemma mod_one (a : R) : a % 1 = 0 :=
 mod_eq_zero.2 (one_dvd _)

src/algebra/group/units.lean

@@ -328,6 +328,17 @@ by rw [divp_eq_iff_mul_eq, divp_mul_eq_mul_divp, divp_eq_iff_mul_eq]
   (x /ₚ ux) * (y /ₚ uy) = (x * y) /ₚ (ux * uy) :=
 by rw [divp_mul_eq_mul_divp, divp_assoc', divp_divp_eq_divp_mul]
 
+variables [subsingleton αˣ] {a b : α}
+
+@[to_additive] lemma eq_one_of_mul_right (h : a * b = 1) : a = 1 :=
+congr_arg units.inv $ subsingleton.elim (units.mk _ _ (by rwa mul_comm) h) 1
+
+@[to_additive] lemma eq_one_of_mul_left (h : a * b = 1) : b = 1 :=
+congr_arg units.inv $ subsingleton.elim (units.mk _ _ h $ by rwa mul_comm) 1
+
+@[simp, to_additive] lemma mul_eq_one : a * b = 1 ↔ a = 1 ∧ b = 1 :=
+⟨λ h, ⟨eq_one_of_mul_right h, eq_one_of_mul_left h⟩, by { rintro ⟨rfl, rfl⟩, exact mul_one _ }⟩
+
 end comm_monoid
 
 /-!

src/algebra/group_with_zero/basic.lean

@@ -156,6 +156,15 @@ lemma mul_left_eq_self₀ : a * b = b ↔ a = 1 ∨ b = 0 :=
 calc a * b = b ↔ a * b = 1 * b : by rw one_mul
      ...       ↔ a = 1 ∨ b = 0 : mul_eq_mul_right_iff
 
+@[simp] lemma mul_eq_left₀ (ha : a ≠ 0) : a * b = a ↔ b = 1 :=
+by rw [iff.comm, ←mul_right_inj' ha, mul_one]
+
+@[simp] lemma mul_eq_right₀ (hb : b ≠ 0) : a * b = b ↔ a = 1 :=
+by rw [iff.comm, ←mul_left_inj' hb, one_mul]
+
+@[simp] lemma left_eq_mul₀ (ha : a ≠ 0) : a = a * b ↔ b = 1 := by rw [eq_comm, mul_eq_left₀ ha]
+@[simp] lemma right_eq_mul₀ (hb : b ≠ 0) : b = a * b ↔ a = 1 := by rw [eq_comm, mul_eq_right₀ hb]
+
 /-- An element of a `cancel_monoid_with_zero` fixed by right multiplication by an element other
 than one must be zero. -/
 theorem eq_zero_of_mul_eq_self_right (h₁ : b ≠ 1) (h₂ : a * b = a) : a = 0 :=
@@ -228,6 +237,14 @@ instance group_with_zero.to_division_monoid : division_monoid G₀ :=
   inv_eq_of_mul := λ a b, inv_eq_of_mul,
   ..‹group_with_zero G₀› }
 
+@[priority 10] -- see Note [lower instance priority]
+instance group_with_zero.to_cancel_monoid_with_zero : cancel_monoid_with_zero G₀ :=
+{ mul_left_cancel_of_ne_zero := λ x y z hx h,
+    by rw [← inv_mul_cancel_left₀ hx y, h, inv_mul_cancel_left₀ hx z],
+  mul_right_cancel_of_ne_zero := λ x y z hy h,
+    by rw [← mul_inv_cancel_right₀ hy x, h, mul_inv_cancel_right₀ hy z],
+  ..‹group_with_zero G₀› }
+
 end group_with_zero
 
 section group_with_zero

src/algebra/group_with_zero/divisibility.lean

@@ -88,3 +88,28 @@ begin
 end
 
 end monoid_with_zero
+
+section cancel_comm_monoid_with_zero
+variables [cancel_comm_monoid_with_zero α] [subsingleton αˣ] {a b : α}
+
+lemma dvd_antisymm : a ∣ b → b ∣ a → a = b :=
+begin
+  rintro ⟨c, rfl⟩ ⟨d, hcd⟩,
+  rw [mul_assoc, eq_comm, mul_right_eq_self₀, mul_eq_one] at hcd,
+  obtain ⟨rfl, -⟩ | rfl := hcd; simp,
+end
+
+attribute [protected] nat.dvd_antisymm --This lemma is in core, so we protect it here
+
+lemma dvd_antisymm' : a ∣ b → b ∣ a → b = a := flip dvd_antisymm
+
+alias dvd_antisymm ← has_dvd.dvd.antisymm
+alias dvd_antisymm' ← has_dvd.dvd.antisymm'
+
+lemma eq_of_forall_dvd (h : ∀ c, a ∣ c ↔ b ∣ c) : a = b :=
+((h _).2 dvd_rfl).antisymm $ (h _).1 dvd_rfl
+
+lemma eq_of_forall_dvd' (h : ∀ c, c ∣ a ↔ c ∣ b) : a = b :=
+((h _).1 dvd_rfl).antisymm $ (h _).2 dvd_rfl
+
+end cancel_comm_monoid_with_zero

src/algebra/order/monoid/canonical/defs.lean

@@ -140,6 +140,8 @@ le_iff_exists_mul.mpr ⟨a, (one_mul _).symm⟩
 @[to_additive] lemma bot_eq_one : (⊥ : α) = 1 :=
 le_antisymm bot_le (one_le ⊥)
 
+--TODO: This is a special case of `mul_eq_one`. We need the instance
+-- `canonically_ordered_monoid α → unique αˣ`
 @[simp, to_additive] lemma mul_eq_one_iff : a * b = 1 ↔ a = 1 ∧ b = 1 :=
 mul_eq_one_iff' (one_le _) (one_le _)
 

src/algebra/ring/boolean_ring.lean

@@ -63,7 +63,7 @@ calc -a = -a + 0      : by rw add_zero
     ... = -a + -a + a : by rw [←neg_add_self, add_assoc]
     ... = a           : by rw [add_self, zero_add]
 
-lemma add_eq_zero : a + b = 0 ↔ a = b :=
+lemma add_eq_zero' : a + b = 0 ↔ a = b :=
 calc a + b = 0 ↔ a = -b : add_eq_zero_iff_eq_neg
            ... ↔ a = b  : by rw neg_eq
 
@@ -82,7 +82,7 @@ by rw [sub_eq_add_neg, add_right_inj, neg_eq]
 
 @[priority 100] -- Note [lower instance priority]
 instance boolean_ring.to_comm_ring : comm_ring α :=
-{ mul_comm := λ a b, by rw [←add_eq_zero, mul_add_mul],
+{ mul_comm := λ a b, by rw [←add_eq_zero', mul_add_mul],
   .. (infer_instance : boolean_ring α) }
 
 end boolean_ring

src/algebra/ring/divisibility.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Yury Kudryashov, Neil Strickland
 -/
 import algebra.divisibility.basic
+import algebra.hom.equiv.basic
 import algebra.ring.defs
 
 /-!
@@ -21,6 +22,8 @@ variables [has_add α] [semigroup α]
 theorem dvd_add [left_distrib_class α] {a b c : α} (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b + c :=
 dvd.elim h₁ (λ d hd, dvd.elim h₂ (λ e he, dvd.intro (d + e) (by simp [left_distrib, hd, he])))
 
+alias dvd_add ← has_dvd.dvd.add
+
 end distrib_semigroup
 
 @[simp] theorem two_dvd_bit0 [semiring α] {a : α} : 2 ∣ bit0 a := ⟨a, bit0_eq_two_mul _⟩
@@ -39,62 +42,50 @@ section semigroup
 
 variables [semigroup α] [has_distrib_neg α] {a b c : α}
 
-theorem dvd_neg_of_dvd (h : a ∣ b) : (a ∣ -b) :=
-let ⟨c, hc⟩ := h in ⟨-c, by simp [hc]⟩
-
-theorem dvd_of_dvd_neg (h : a ∣ -b) : (a ∣ b) :=
-let t := dvd_neg_of_dvd h in by rwa neg_neg at t
-
-/-- An element a of a semigroup with a distributive negation divides the negation of an element b
-iff a divides b. -/
-@[simp] lemma dvd_neg (a b : α) : (a ∣ -b) ↔ (a ∣ b) :=
-⟨dvd_of_dvd_neg, dvd_neg_of_dvd⟩
-
-theorem neg_dvd_of_dvd (h : a ∣ b) : -a ∣ b :=
-let ⟨c, hc⟩ := h in ⟨-c, by simp [hc]⟩
+/-- An element `a` of a semigroup with a distributive negation divides the negation of an element
+`b` iff `a` divides `b`. -/
+@[simp] lemma dvd_neg : a ∣ -b ↔ a ∣ b := (equiv.neg _).exists_congr_left.trans $ by simpa
 
-theorem dvd_of_neg_dvd (h : -a ∣ b) : a ∣ b :=
-let t := neg_dvd_of_dvd h in by rwa neg_neg at t
+/-- The negation of an element `a` of a semigroup with a distributive negation divides another
+element `b` iff `a` divides `b`. -/
+@[simp] lemma neg_dvd : -a ∣ b ↔ a ∣ b := (equiv.neg _).exists_congr_left.trans $ by simpa
 
-/-- The negation of an element a of a semigroup with a distributive negation divides
-another element b iff a divides b. -/
-@[simp] lemma neg_dvd (a b : α) : (-a ∣ b) ↔ (a ∣ b) :=
-⟨dvd_of_neg_dvd, neg_dvd_of_dvd⟩
+alias neg_dvd ↔ has_dvd.dvd.of_neg_left has_dvd.dvd.neg_left
+alias dvd_neg ↔ has_dvd.dvd.of_neg_right has_dvd.dvd.neg_right
 
 end semigroup
 
 section non_unital_ring
 variables [non_unital_ring α] {a b c : α}
 
 theorem dvd_sub (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b - c :=
-by { rw sub_eq_add_neg, exact dvd_add h₁ (dvd_neg_of_dvd h₂) }
+by simpa only [←sub_eq_add_neg] using h₁.add h₂.neg_right
 
-theorem dvd_add_iff_left (h : a ∣ c) : a ∣ b ↔ a ∣ b + c :=
-⟨λh₂, dvd_add h₂ h, λH, by have t := dvd_sub H h; rwa add_sub_cancel at t⟩
+alias dvd_sub ← has_dvd.dvd.sub
 
-theorem dvd_add_iff_right (h : a ∣ b) : a ∣ c ↔ a ∣ b + c :=
-by rw add_comm; exact dvd_add_iff_left h
-
-/-- If an element a divides another element c in a commutative ring, a divides the sum of another
-  element b with c iff a divides b. -/
+/-- If an element `a` divides another element `c` in a ring, `a` divides the sum of another element
+`b` with `c` iff `a` divides `b`. -/
 theorem dvd_add_left (h : a ∣ c) : a ∣ b + c ↔ a ∣ b :=
-(dvd_add_iff_left h).symm
+⟨λ H, by simpa only [add_sub_cancel] using dvd_sub H h, λ h₂, dvd_add h₂ h⟩
 
-/-- If an element a divides another element b in a commutative ring, a divides the sum of b and
-  another element c iff a divides c. -/
-theorem dvd_add_right (h : a ∣ b) : a ∣ b + c ↔ a ∣ c :=
-(dvd_add_iff_right h).symm
+/-- If an element `a` divides another element `b` in a ring, `a` divides the sum of `b` and another
+element `c` iff `a` divides `c`. -/
+theorem dvd_add_right (h : a ∣ b) : a ∣ b + c ↔ a ∣ c := by rw add_comm; exact dvd_add_left h
 
-lemma dvd_iff_dvd_of_dvd_sub {a b c : α} (h : a ∣ (b - c)) : (a ∣ b ↔ a ∣ c) :=
-begin
-  split,
-  { intro h',
-    convert dvd_sub h' h,
-    exact eq.symm (sub_sub_self b c) },
-  { intro h',
-    convert dvd_add h h',
-    exact eq_add_of_sub_eq rfl }
-end
+/-- If an element `a` divides another element `c` in a ring, `a` divides the difference of another
+element `b` with `c` iff `a` divides `b`. -/
+theorem dvd_sub_left (h : a ∣ c) : a ∣ b - c ↔ a ∣ b :=
+by simpa only [←sub_eq_add_neg] using dvd_add_left (dvd_neg.2 h)
+
+/-- If an element `a` divides another element `b` in a ring, `a` divides the difference of `b` and
+another element `c` iff `a` divides `c`. -/
+theorem dvd_sub_right (h : a ∣ b) : a ∣ b - c ↔ a ∣ c :=
+by rw [sub_eq_add_neg, dvd_add_right h, dvd_neg]
+
+lemma dvd_iff_dvd_of_dvd_sub (h : a ∣ b - c) : a ∣ b ↔ a ∣ c :=
+by rw [←sub_add_cancel b c, dvd_add_right h]
+
+lemma dvd_sub_comm : a ∣ b - c ↔ a ∣ c - b := by rw [←dvd_neg, neg_sub]
 
 lemma dvd_sub_comm : a ∣ b - c ↔ a ∣ c - b := by rw [←dvd_neg, neg_sub]
 
@@ -103,7 +94,7 @@ end non_unital_ring
 section ring
 variables [ring α] {a b c : α}
 
-theorem two_dvd_bit1 : 2 ∣ bit1 a ↔ (2 : α) ∣ 1 := (dvd_add_iff_right (@two_dvd_bit0 _ _ a)).symm
+theorem two_dvd_bit1 : 2 ∣ bit1 a ↔ (2 : α) ∣ 1 := dvd_add_right two_dvd_bit0
 
 /-- An element a divides the sum a + b if and only if a divides b.-/
 @[simp] lemma dvd_add_self_left {a b : α} : a ∣ a + b ↔ a ∣ b :=
@@ -113,6 +104,12 @@ dvd_add_right (dvd_refl a)
 @[simp] lemma dvd_add_self_right {a b : α} : a ∣ b + a ↔ a ∣ b :=
 dvd_add_left (dvd_refl a)
 
+/-- An element `a` divides the difference `a - b` if and only if `a` divides `b`. -/
+@[simp] lemma dvd_sub_self_left : a ∣ a - b ↔ a ∣ b := dvd_sub_right dvd_rfl
+
+/-- An element `a` divides the difference `b - a` if and only if `a` divides `b`. -/
+@[simp] lemma dvd_sub_self_right : a ∣ b - a ↔ a ∣ b := dvd_sub_left dvd_rfl
+
 end ring
 
 section non_unital_comm_ring

src/data/int/dvd/basic.lean

@@ -52,22 +52,6 @@ eq_one_of_dvd_one H ⟨b, H'.symm⟩
 theorem eq_one_of_mul_eq_one_left {a b : ℤ} (H : 0 ≤ b) (H' : a * b = 1) : b = 1 :=
 eq_one_of_mul_eq_one_right H (by rw [mul_comm, H'])
 
-lemma of_nat_dvd_of_dvd_nat_abs {a : ℕ} : ∀ {z : ℤ} (haz : a ∣ z.nat_abs), ↑a ∣ z
-| (int.of_nat _) haz := int.coe_nat_dvd.2 haz
-| -[1+k] haz :=
-  begin
-    change ↑a ∣ -(k+1 : ℤ),
-    apply dvd_neg_of_dvd,
-    apply int.coe_nat_dvd.2,
-    exact haz
-  end
-
-lemma dvd_nat_abs_of_of_nat_dvd {a : ℕ} : ∀ {z : ℤ} (haz : ↑a ∣ z), a ∣ z.nat_abs
-| (int.of_nat _) haz := int.coe_nat_dvd.1 (int.dvd_nat_abs.2 haz)
-| -[1+k] haz :=
-  have haz' : (↑a:ℤ) ∣ (↑(k+1):ℤ), from dvd_of_dvd_neg haz,
-  int.coe_nat_dvd.1 haz'
-
 theorem dvd_antisymm {a b : ℤ} (H1 : 0 ≤ a) (H2 : 0 ≤ b) : a ∣ b → b ∣ a → a = b :=
 begin
   rw [← abs_of_nonneg H1, ← abs_of_nonneg H2, abs_eq_nat_abs, abs_eq_nat_abs],

src/data/int/dvd/pow.lean

@@ -23,23 +23,12 @@ theorem sign_pow_bit1 (k : ℕ) : ∀ n : ℤ, n.sign ^ (bit1 k) = n.sign
 | 0       := zero_pow (nat.zero_lt_bit1 k)
 | -[1+ n] := (neg_pow_bit1 1 k).trans (congr_arg (λ x, -x) (one_pow (bit1 k)))
 
+--TODO: Do we really need this lemma?
 lemma pow_dvd_of_le_of_pow_dvd {p m n : ℕ} {k : ℤ} (hmn : m ≤ n) (hdiv : ↑(p ^ n) ∣ k) :
   ↑(p ^ m) ∣ k :=
-begin
-  induction k,
-  { apply int.coe_nat_dvd.2,
-    apply pow_dvd_of_le_of_pow_dvd hmn,
-    apply int.coe_nat_dvd.1 hdiv },
-  change -[1+k] with -(↑(k+1) : ℤ),
-  apply dvd_neg_of_dvd,
-  apply int.coe_nat_dvd.2,
-  apply pow_dvd_of_le_of_pow_dvd hmn,
-  apply int.coe_nat_dvd.1,
-  apply dvd_of_dvd_neg,
-  exact hdiv,
-end
+(pow_dvd_pow _ hmn).nat_cast.trans hdiv
 
 lemma dvd_of_pow_dvd {p k : ℕ} {m : ℤ} (hk : 1 ≤ k) (hpk : ↑(p^k) ∣ m) : ↑p ∣ m :=
-by rw ←pow_one p; exact pow_dvd_of_le_of_pow_dvd hk hpk
+(dvd_pow_self _ $ pos_iff_ne_zero.1 hk).nat_cast.trans hpk
 
 end int

src/data/int/order/basic.lean

@@ -525,7 +525,7 @@ theorem neg_div_of_dvd : ∀ {a b : ℤ} (H : b ∣ a), -a / b = -(a / b)
 
 lemma sub_div_of_dvd (a : ℤ) {b c : ℤ} (hcb : c ∣ b) : (a - b) / c = a / c - b / c :=
 begin
-  rw [sub_eq_add_neg, sub_eq_add_neg, int.add_div_of_dvd_right ((dvd_neg c b).mpr hcb)],
+  rw [sub_eq_add_neg, sub_eq_add_neg, int.add_div_of_dvd_right hcb.neg_right],
   congr,
   exact neg_div_of_dvd hcb,
 end

src/data/nat/gcd/basic.lean

@@ -266,6 +266,9 @@ dvd_antisymm
 theorem lcm_ne_zero {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) : lcm m n ≠ 0 :=
 by { intro h, simpa [h, hm, hn] using gcd_mul_lcm m n, }
 
+lemma lcm_pos {m n : ℕ} : 0 < m → 0 < n → 0 < m.lcm n :=
+by { simp_rw pos_iff_ne_zero, exact lcm_ne_zero }
+
 /-!
 ### `coprime`
 

src/data/nat/order/basic.lean

@@ -65,7 +65,7 @@ instance : canonically_linear_ordered_add_monoid ℕ :=
 { .. (infer_instance : canonically_ordered_add_monoid ℕ),
   .. nat.linear_order }
 
-variables {m n k l : ℕ}
+variables {a b m n k l : ℕ}
 namespace nat
 
 /-! ### Equalities and inequalities involving zero and one -/
@@ -94,7 +94,6 @@ lemma eq_zero_of_mul_le (hb : 2 ≤ n) (h : n * m ≤ m) : m = 0 :=
 eq_zero_of_double_le $ le_trans (nat.mul_le_mul_right _ hb) h
 
 lemma zero_max : max 0 n = n := max_eq_right (zero_le _)
-
 @[simp] lemma min_eq_zero_iff : min m n = 0 ↔ m = 0 ∨ n = 0 :=
 begin
   split,
@@ -243,17 +242,6 @@ lemma sub_succ' (m n : ℕ) : m - n.succ = m - n - 1 := rfl
 
 /-! ### `mul` -/
 
-lemma mul_eq_one_iff : ∀ {m n : ℕ}, m * n = 1 ↔ m = 1 ∧ n = 1
-| 0     0     := dec_trivial
-| 0     1     := dec_trivial
-| 1     0     := dec_trivial
-| (m+2) 0     := by simp
-| 0     (n+2) := by simp
-| (m+1) (n+1) := ⟨
-  λ h, by simp only [add_mul, mul_add, mul_add, one_mul, mul_one,
-    (add_assoc _ _ _).symm, nat.succ_inj', add_eq_zero_iff] at h; simp [h.1.2, h.2],
-  λ h, by simp only [h, mul_one]⟩
-
 lemma succ_mul_pos (m : ℕ) (hn : 0 < n) : 0 < (succ m) * n := mul_pos (succ_pos m) hn
 
 theorem mul_self_le_mul_self (h : m ≤ n) : m * m ≤ n * n := mul_le_mul h h (zero_le _) (zero_le _)

src/data/nat/order/lemmas.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 import data.nat.order.basic
+import data.nat.units
 import data.set.basic
 import algebra.ring.divisibility
 import algebra.group_with_zero.divisibility