rw [Nat.succ_le_iff]
case a.a.mp.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
i : ℕ
hi : i < d
j : ℕ
hj : j * d ≤ s - i - 1
⊢ 1 ≤ s - i
case a.a.mp.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s d : ℕ
hd : d ≠ 0
h : d ≤ s
i : ℕ
hi : i < d
j : ℕ
hj : j * d ≤ s - i - 1
⊢ 0 < s - i