[GOAL]
a b m n k : ℕ
S : Set ℕ
⊢ S = Set.univ → 0 ∈ S ∧ ∀ (k : ℕ), k ∈ S → k + 1 ∈ S
[PROOFSTEP]
rintro rfl
[GOAL]
a b m n k : ℕ
⊢ 0 ∈ Set.univ ∧ ∀ (k : ℕ), k ∈ Set.univ → k + 1 ∈ Set.univ
[PROOFSTEP]
simp
[GOAL]
a✝ b m n✝ k n d : ℕ
hnd : d ∣ n
a : ℕ
⊢ a < n / d ↔ d * a < n
[PROOFSTEP]
rcases d.eq_zero_or_pos with (rfl | hd0)
[GOAL]
case inl
a✝ b m n✝ k n a : ℕ
hnd : 0 ∣ n
⊢ a < n / 0 ↔ 0 * a < n
[PROOFSTEP]
simp [zero_dvd_iff.mp hnd]
[GOAL]
case inr
a✝ b m n✝ k n d : ℕ
hnd : d ∣ n
a : ℕ
hd0 : d > 0
⊢ a < n / d ↔ d * a < n
[PROOFSTEP]
rw [← mul_lt_mul_left hd0, ← Nat.eq_mul_of_div_eq_right hnd rfl]
[GOAL]
a b m n✝ k n d : ℕ
⊢ d * (n / d) = n ↔ d * (n / d) = d * (n / d) + n % d
[PROOFSTEP]
rw [div_add_mod]
[GOAL]
a b m n✝ k n d : ℕ
⊢ d * (n / d) = d * (n / d) + n % d ↔ d ∣ n
[PROOFSTEP]
rw [self_eq_add_right, dvd_iff_mod_eq_zero]
  -- porting note: new lemma
[GOAL]
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
⊢ n / x = n / y ↔ x = y
[PROOFSTEP]
constructor
[GOAL]
case mp
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
⊢ n / x = n / y → x = y
[PROOFSTEP]
intro h
[GOAL]
case mp
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
h : n / x = n / y
⊢ x = y
[PROOFSTEP]
rw [← mul_right_inj' hn]
[GOAL]
case mp
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
h : n / x = n / y
⊢ n * x = n * y
[PROOFSTEP]
apply Nat.eq_mul_of_div_eq_left (dvd_mul_of_dvd_left hy x)
[GOAL]
case mp
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
h : n / x = n / y
⊢ n * x / y = n
[PROOFSTEP]
rw [eq_comm, mul_comm, Nat.mul_div_assoc _ hy]
[GOAL]
case mp
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
h : n / x = n / y
⊢ n = x * (n / y)
[PROOFSTEP]
exact Nat.eq_mul_of_div_eq_right hx h
[GOAL]
case mpr
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
⊢ x = y → n / x = n / y
[PROOFSTEP]
intro h
[GOAL]
case mpr
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
h : x = y
⊢ n / x = n / y
[PROOFSTEP]
rw [h]
[GOAL]
a✝ b✝ m n k a b : ℕ
hb : 0 < b
h : a / b = 0
⊢ a < b
[PROOFSTEP]
rw [← mod_add_div a b, h, mul_zero, add_zero]
[GOAL]
a✝ b✝ m n k a b : ℕ
hb : 0 < b
h : a / b = 0
⊢ a % b < b
[PROOFSTEP]
exact mod_lt _ hb
[GOAL]
a✝ b✝ m n k a b : ℕ
hb : 0 < b
h : a < b
⊢ a / b = 0
[PROOFSTEP]
rw [← mul_right_inj' hb.ne', ← @add_left_cancel_iff _ _ _ (a % b), mod_add_div, mod_eq_of_lt h, mul_zero, add_zero]
[GOAL]
a b m n✝ k n : ℕ
⊢ ¬2 ∣ bit1 n
[PROOFSTEP]
rw [bit1, Nat.dvd_add_right two_dvd_bit0, Nat.dvd_one]
  -- Porting note: was `cc`
[GOAL]
a b m n✝ k n : ℕ
⊢ ¬2 = 1
[PROOFSTEP]
decide
[GOAL]
a b m✝ n✝ k✝ k m n : ℕ
h₁ : k ∣ m
h₂ : k ∣ n
⊢ k ∣ m - n
[PROOFSTEP]
cases' le_total n m with H H
[GOAL]
case inl
a b m✝ n✝ k✝ k m n : ℕ
h₁ : k ∣ m
h₂ : k ∣ n
H : n ≤ m
⊢ k ∣ m - n
[PROOFSTEP]
exact dvd_sub H h₁ h₂
[GOAL]
case inr
a b m✝ n✝ k✝ k m n : ℕ
h₁ : k ∣ m
h₂ : k ∣ n
H : m ≤ n
⊢ k ∣ m - n
[PROOFSTEP]
rw [tsub_eq_zero_iff_le.mpr H]
[GOAL]
case inr
a b m✝ n✝ k✝ k m n : ℕ
h₁ : k ∣ m
h₂ : k ∣ n
H : m ≤ n
⊢ k ∣ 0
[PROOFSTEP]
exact dvd_zero k
[GOAL]
a✝ b m n k a : ℕ
⊢ (a + 1) / 0 = a / 0 + if 0 ∣ a + 1 then 1 else 0
[PROOFSTEP]
simp
[GOAL]
a b m n k : ℕ
⊢ (0 + 1) / 1 = 0 / 1 + if 1 ∣ 0 + 1 then 1 else 0
[PROOFSTEP]
simp
[GOAL]
a b✝ m n k b : ℕ
⊢ (0 + 1) / (b + 2) = 0 / (b + 2) + if b + 2 ∣ 0 + 1 then 1 else 0
[PROOFSTEP]
have hb2 : b + 2 > 1 := by simp
[GOAL]
a b✝ m n k b : ℕ
⊢ b + 2 > 1
[PROOFSTEP]
simp
[GOAL]
a b✝ m n k b : ℕ
hb2 : b + 2 > 1
⊢ (0 + 1) / (b + 2) = 0 / (b + 2) + if b + 2 ∣ 0 + 1 then 1 else 0
[PROOFSTEP]
simp [ne_of_gt hb2, div_eq_of_lt hb2]
[GOAL]
a✝ b✝ m n k a b : ℕ
⊢ (a + 1 + 1) / (b + 1) = (a + 1) / (b + 1) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
rw [Nat.div_eq]
[GOAL]
a✝ b✝ m n k a b : ℕ
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (a + 1) / (b + 1) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
conv_rhs => rw [Nat.div_eq]
[GOAL]
a✝ b✝ m n k a b : ℕ
| (a + 1) / (b + 1) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
rw [Nat.div_eq]
[GOAL]
a✝ b✝ m n k a b : ℕ
| (a + 1) / (b + 1) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
rw [Nat.div_eq]
[GOAL]
a✝ b✝ m n k a b : ℕ
| (a + 1) / (b + 1) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
rw [Nat.div_eq]
[GOAL]
a✝ b✝ m n k a b : ℕ
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
by_cases hb_eq_a : b = a + 1
[GOAL]
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : b = a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
simp [hb_eq_a, le_refl]
[GOAL]
case neg
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
by_cases hb_le_a1 : b ≤ a + 1
[GOAL]
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
have hb_le_a : b ≤ a := le_of_lt_succ (lt_of_le_of_ne hb_le_a1 hb_eq_a)
[GOAL]
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
have h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 := ⟨succ_pos _, (add_le_add_iff_right _).2 hb_le_a1⟩
[GOAL]
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
have h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1 := ⟨succ_pos _, (add_le_add_iff_right _).2 hb_le_a⟩
[GOAL]
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
have dvd_iff : b + 1 ∣ a - b + 1 ↔ b + 1 ∣ a + 1 + 1 := by
  rw [Nat.dvd_add_iff_left (dvd_refl (b + 1)), ← add_tsub_add_eq_tsub_right a 1 b, add_comm (_ - _), add_assoc,
    tsub_add_cancel_of_le (succ_le_succ hb_le_a), add_comm 1]
[GOAL]
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1
⊢ b + 1 ∣ a - b + 1 ↔ b + 1 ∣ a + 1 + 1
[PROOFSTEP]
rw [Nat.dvd_add_iff_left (dvd_refl (b + 1)), ← add_tsub_add_eq_tsub_right a 1 b, add_comm (_ - _), add_assoc,
  tsub_add_cancel_of_le (succ_le_succ hb_le_a), add_comm 1]
[GOAL]
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1
dvd_iff : b + 1 ∣ a - b + 1 ↔ b + 1 ∣ a + 1 + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
have wf : a - b < a + 1 := lt_succ_of_le tsub_le_self
[GOAL]
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1
dvd_iff : b + 1 ∣ a - b + 1 ↔ b + 1 ∣ a + 1 + 1
wf : a - b < a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
rw [if_pos h₁, if_pos h₂, @add_tsub_add_eq_tsub_right, ← tsub_add_eq_add_tsub hb_le_a,
  have := wf
  succ_div (a - b),
  @add_tsub_add_eq_tsub_right]
[GOAL]
case pos
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : b ≤ a + 1
hb_le_a : b ≤ a
h₁ : 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1
h₂ : 0 < b + 1 ∧ b + 1 ≤ a + 1
dvd_iff : b + 1 ∣ a - b + 1 ↔ b + 1 ∣ a + 1 + 1
wf : a - b < a + 1
⊢ ((a - b) / (b + 1) + if b + 1 ∣ a - b + 1 then 1 else 0) + 1 =
    (a - b) / (b + 1) + 1 + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
simp [dvd_iff, succ_eq_add_one, add_comm 1, add_assoc]
[GOAL]
case neg
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : ¬b ≤ a + 1
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
have hba : ¬b ≤ a := not_le_of_gt (lt_trans (lt_succ_self a) (lt_of_not_ge hb_le_a1))
[GOAL]
case neg
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : ¬b ≤ a + 1
hba : ¬b ≤ a
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
have hb_dvd_a : ¬b + 1 ∣ a + 2 := fun h => hb_le_a1 (le_of_succ_le_succ (le_of_dvd (succ_pos _) h))
[GOAL]
case neg
a✝ b✝ m n k a b : ℕ
hb_eq_a : ¬b = a + 1
hb_le_a1 : ¬b ≤ a + 1
hba : ¬b ≤ a
hb_dvd_a : ¬b + 1 ∣ a + 2
⊢ (if 0 < b + 1 ∧ b + 1 ≤ a + 1 + 1 then (a + 1 + 1 - (b + 1)) / (b + 1) + 1 else 0) =
    (if 0 < b + 1 ∧ b + 1 ≤ a + 1 then (a + 1 - (b + 1)) / (b + 1) + 1 else 0) + if b + 1 ∣ a + 1 + 1 then 1 else 0
[PROOFSTEP]
simp [hba, hb_le_a1, hb_dvd_a]
[GOAL]
a✝ b✝ m n k a b : ℕ
hba : b ∣ a + 1
⊢ (a + 1) / b = a / b + 1
[PROOFSTEP]
rw [succ_div, if_pos hba]
[GOAL]
a✝ b✝ m n k a b : ℕ
hba : ¬b ∣ a + 1
⊢ (a + 1) / b = a / b
[PROOFSTEP]
rw [succ_div, if_neg hba, add_zero]
[GOAL]
a✝ b✝ m n k a b c : ℕ
h : a * b ∣ c
ha : a = 0
⊢ b ∣ c / a
[PROOFSTEP]
simp [ha]
[GOAL]
a✝ b✝ m n k a b c : ℕ
h : a * b ∣ c
ha✝ : ¬a = 0
ha : 0 < a
h1 : ∃ d, c = a * b * d
d : ℕ
hd : c = a * b * d
⊢ c = a * (b * d)
[PROOFSTEP]
simpa [mul_assoc] using hd
[GOAL]
a✝ b✝ m n k a b c x✝¹ x✝ : ℕ
dvd : x✝¹ ∣ 0
dvd2 : 0 ∣ x✝
⊢ x✝ / (0 / x✝¹) / x✝¹ = x✝ / 0
[PROOFSTEP]
simp
[GOAL]
a✝¹ b✝ m n k a✝ b c a x✝ : ℕ
dvd : 0 ∣ a + 1
dvd2 : a + 1 ∣ x✝
⊢ x✝ / ((a + 1) / 0) / 0 = x✝ / (a + 1)
[PROOFSTEP]
simp at dvd 
[GOAL]
a✝¹ b✝ m n k a✝ b c✝ a c x✝ : ℕ
dvd : c + 1 ∣ a + 1
dvd2 : a + 1 ∣ x✝
⊢ x✝ / ((a + 1) / (c + 1)) / (c + 1) = x✝ / (a + 1)
[PROOFSTEP]
have a_split : a + 1 ≠ 0 := succ_ne_zero a
[GOAL]
a✝¹ b✝ m n k a✝ b c✝ a c x✝ : ℕ
dvd : c + 1 ∣ a + 1
dvd2 : a + 1 ∣ x✝
a_split : a + 1 ≠ 0
⊢ x✝ / ((a + 1) / (c + 1)) / (c + 1) = x✝ / (a + 1)
[PROOFSTEP]
have c_split : c + 1 ≠ 0 := succ_ne_zero c
[GOAL]
a✝¹ b✝ m n k a✝ b c✝ a c x✝ : ℕ
dvd : c + 1 ∣ a + 1
dvd2 : a + 1 ∣ x✝
a_split : a + 1 ≠ 0
c_split : c + 1 ≠ 0
⊢ x✝ / ((a + 1) / (c + 1)) / (c + 1) = x✝ / (a + 1)
[PROOFSTEP]
rcases dvd2 with ⟨k, rfl⟩
[GOAL]
case intro
a✝¹ b✝ m n k✝ a✝ b c✝ a c : ℕ
dvd : c + 1 ∣ a + 1
a_split : a + 1 ≠ 0
c_split : c + 1 ≠ 0
k : ℕ
⊢ (a + 1) * k / ((a + 1) / (c + 1)) / (c + 1) = (a + 1) * k / (a + 1)
[PROOFSTEP]
rcases dvd with ⟨k2, pr⟩
[GOAL]
case intro.intro
a✝¹ b✝ m n k✝ a✝ b c✝ a c : ℕ
a_split : a + 1 ≠ 0
c_split : c + 1 ≠ 0
k k2 : ℕ
pr : a + 1 = (c + 1) * k2
⊢ (a + 1) * k / ((a + 1) / (c + 1)) / (c + 1) = (a + 1) * k / (a + 1)
[PROOFSTEP]
have k2_nonzero : k2 ≠ 0 := fun k2_zero => by simp [k2_zero] at pr 
[GOAL]
a✝¹ b✝ m n k✝ a✝ b c✝ a c : ℕ
a_split : a + 1 ≠ 0
c_split : c + 1 ≠ 0
k k2 : ℕ
pr : a + 1 = (c + 1) * k2
k2_zero : k2 = 0
⊢ False
[PROOFSTEP]
simp [k2_zero] at pr 
[GOAL]
case intro.intro
a✝¹ b✝ m n k✝ a✝ b c✝ a c : ℕ
a_split : a + 1 ≠ 0
c_split : c + 1 ≠ 0
k k2 : ℕ
pr : a + 1 = (c + 1) * k2
k2_nonzero : k2 ≠ 0
⊢ (a + 1) * k / ((a + 1) / (c + 1)) / (c + 1) = (a + 1) * k / (a + 1)
[PROOFSTEP]
rw [Nat.mul_div_cancel_left k (Nat.pos_of_ne_zero a_split), pr, Nat.mul_div_cancel_left k2 (Nat.pos_of_ne_zero c_split),
  Nat.mul_comm ((c + 1) * k2) k, ← Nat.mul_assoc k (c + 1) k2, Nat.mul_div_cancel _ (Nat.pos_of_ne_zero k2_nonzero),
  Nat.mul_div_cancel _ (Nat.pos_of_ne_zero c_split)]
[GOAL]
a b m n k : ℕ
h : a < b + n
⊢ n ∣ a → n ∣ b → a ≤ b
[PROOFSTEP]
rintro ⟨a, rfl⟩
  ⟨b, rfl⟩
      -- porting note: Needed to give an explicit argument to `mul_add_one`
[GOAL]
case intro.intro
m n k a b : ℕ
h : n * a < n * b + n
⊢ n * a ≤ n * b
[PROOFSTEP]
rw [← mul_add_one n] at h 
[GOAL]
case intro.intro
m n k a b : ℕ
h : n * a < n * (b + 1)
⊢ n * a ≤ n * b
[PROOFSTEP]
exact mul_le_mul_left' (lt_succ_iff.1 <| lt_of_mul_lt_mul_left h bot_le) _
[GOAL]
a b m✝ n✝ k m n : ℕ
⊢ m % n / n = 0
[PROOFSTEP]
cases n
[GOAL]
case zero
a b m✝ n k m : ℕ
⊢ m % zero / zero = 0
[PROOFSTEP]
exact (m % 0).div_zero
[GOAL]
case succ
a b m✝ n k m n✝ : ℕ
⊢ m % succ n✝ / succ n✝ = 0
[PROOFSTEP]
case succ n => exact Nat.div_eq_zero (m.mod_lt n.succ_pos)
[GOAL]
a b m✝ n✝ k m n : ℕ
⊢ m % succ n / succ n = 0
[PROOFSTEP]
case succ n => exact Nat.div_eq_zero (m.mod_lt n.succ_pos)
[GOAL]
a b m✝ n✝ k m n : ℕ
⊢ m % succ n / succ n = 0
[PROOFSTEP]
exact Nat.div_eq_zero (m.mod_lt n.succ_pos)
[GOAL]
a✝ b m n✝ k n a : ℕ
ha : 0 < a
⊢ (∃ k, a * k < n ∧ n < a * (k + 1)) ↔ ¬a ∣ n
[PROOFSTEP]
refine'
  ⟨fun ⟨k, hk1, hk2⟩ => not_dvd_of_between_consec_multiples hk1 hk2, fun han =>
    ⟨n / a, ⟨lt_of_le_of_ne (mul_div_le n a) _, lt_mul_div_succ _ ha⟩⟩⟩
[GOAL]
a✝ b m n✝ k n a : ℕ
ha : 0 < a
han : ¬a ∣ n
⊢ a * (n / a) ≠ n
[PROOFSTEP]
exact mt (Dvd.intro (n / a)) han
[GOAL]
a b m✝ n✝¹ k m n✝ : ℕ
h : m = n✝
n : ℕ
⊢ m ∣ n ↔ n✝ ∣ n
[PROOFSTEP]
rw [h]
[GOAL]
a b m✝ n✝¹ k m n✝ : ℕ
h : m = n✝
n : ℕ
⊢ n ∣ m ↔ n ∣ n✝
[PROOFSTEP]
rw [h]
[GOAL]
a✝ b✝ m n k a b d : ℕ
hdb : d ∣ b
h : a < b
⊢ a / d < b / d
[PROOFSTEP]
rw [Nat.lt_div_iff_mul_lt hdb]
[GOAL]
a✝ b✝ m n k a b d : ℕ
hdb : d ∣ b
h : a < b
⊢ d * (a / d) < b
[PROOFSTEP]
exact lt_of_le_of_lt (mul_div_le a d) h
