no goals
k x y : Nat
k0 : 0 < k
⊢ x ≤ y / k ↔ x * k ≤ y
induction y, k using mod.inductionOn generalizing x with
  (rw [div_eq]; simp [h]; cases x with simp [zero_le] | succ x => ?_)
| base y k h =>
  simp [not_succ_le_zero x, succ_mul, Nat.add_comm]
  refine Nat.lt_of_lt_of_le ?_ (Nat.le_add_right ..)
  exact Nat.not_le.1 fun h' => h ⟨k0, h'⟩
| ind y k h IH =>
  rw [← add_one, Nat.add_le_add_iff_le_right, IH k0, succ_mul,
      ← Nat.add_sub_cancel (x*k) k, Nat.sub_le_sub_right_iff h.2, Nat.add_sub_cancel]
case ind
y k : Nat
h : 0 < k ∧ k ≤ y
IH : ∀ {x : Nat}, 0 < k → (x ≤ (y - k) / k ↔ x * k ≤ y - k)
x : Nat
k0 : 0 < k
⊢ (x ≤ if 0 < k ∧ k ≤ y then (y - k) / k + 1 else 0) ↔ x * k ≤ y
case ind
y k : Nat
h : 0 < k ∧ k ≤ y
IH : ∀ {x : Nat}, 0 < k → (x ≤ (y - k) / k ↔ x * k ≤ y - k)
x : Nat
k0 : 0 < k
⊢ x ≤ y / k ↔ x * k ≤ y
rw [div_eq]
case ind
y k : Nat
h : 0 < k ∧ k ≤ y
IH : ∀ {x : Nat}, 0 < k → (x ≤ (y - k) / k ↔ x * k ≤ y - k)
x : Nat
k0 : 0 < k
⊢ x ≤ (y - k) / k + 1 ↔ x * k ≤ y
case ind
y k : Nat
h : 0 < k ∧ k ≤ y
IH : ∀ {x : Nat}, 0 < k → (x ≤ (y - k) / k ↔ x * k ≤ y - k)
x : Nat
k0 : 0 < k
⊢ (x ≤ if 0 < k ∧ k ≤ y then (y - k) / k + 1 else 0) ↔ x * k ≤ y
simp [h]
case ind.succ
y k : Nat
h : 0 < k ∧ k ≤ y
IH : ∀ {x : Nat}, 0 < k → (x ≤ (y - k) / k ↔ x * k ≤ y - k)
k0 : 0 < k
x : Nat
⊢ succ x ≤ (y - k) / k + 1 ↔ succ x * k ≤ y
case ind
y k : Nat
h : 0 < k ∧ k ≤ y
IH : ∀ {x : Nat}, 0 < k → (x ≤ (y - k) / k ↔ x * k ≤ y - k)
x : Nat
k0 : 0 < k
⊢ x ≤ (y - k) / k + 1 ↔ x * k ≤ y
cases x with simp [zero_le] | succ x => ?_
case base.succ
y k : Nat
h : ¬(0 < k ∧ k ≤ y)
k0 : 0 < k
x : Nat
⊢ y < k + x * k
case base.succ
y k : Nat
h : ¬(0 < k ∧ k ≤ y)
k0 : 0 < k
x : Nat
⊢ y < succ x * k
simp [not_succ_le_zero x, succ_mul, Nat.add_comm]
case base.succ
y k : Nat
h : ¬(0 < k ∧ k ≤ y)
k0 : 0 < k
x : Nat
⊢ y < k
case base.succ
y k : Nat
h : ¬(0 < k ∧ k ≤ y)
k0 : 0 < k
x : Nat
⊢ y < k + x * k
refine Nat.lt_of_lt_of_le ?_ (Nat.le_add_right ..)
no goals
case base.succ
y k : Nat
h : ¬(0 < k ∧ k ≤ y)
k0 : 0 < k
x : Nat
⊢ y < k
exact Nat.not_le.1 fun h' => h ⟨k0, h'⟩
no goals
case ind.succ
y k : Nat
h : 0 < k ∧ k ≤ y
IH : ∀ {x : Nat}, 0 < k → (x ≤ (y - k) / k ↔ x * k ≤ y - k)
k0 : 0 < k
x : Nat
⊢ succ x ≤ (y - k) / k + 1 ↔ succ x * k ≤ y
rw [← add_one, Nat.add_le_add_iff_le_right, IH k0, succ_mul,
    ← Nat.add_sub_cancel (x*k) k, Nat.sub_le_sub_right_iff h.2, Nat.add_sub_cancel]