rw [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hi, eq_self_iff_true, and_true_iff, ←
  Nat.lt_sub_iff_add_lt', mul_comm]
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 ≤ (s - i - 1) / d
⊢ i + d * j < s ∧ (i + d * j) % d = 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 ≤ (s - i - 1) / d
⊢ j * d < s - i