rwa [Nat.le_div_iff_mul_le' hd.bot_lt, Nat.le_sub_iff_add_le, Nat.le_sub_iff_add_le',
  ← add_assoc, mul_comm, Nat.mod_add_div, Nat.add_one_le_iff]
case a.a.mpr.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
j : ℕ
hj : j < s
hi : j % d < d
⊢ j / d ≤ (s - j % d - 1) / d
case a.a.mpr.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
j : ℕ
hj : j < s
hi : j % d < d
⊢ j % d ≤ s

case a.a.mpr.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
j : ℕ
hj : j < s
hi : j % d < d
⊢ 1 ≤ s - j % d