rw [add_comm, add_comm _ d] at ht
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : (t + 1) * a + c = (t + 1) * b + d
mc : c % (t + 1) = c
md : d % (t + 1) = d
⊢ a = b ∧ c = d
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : c + (t + 1) * a = d + (t + 1) * b
mc : c % (t + 1) = c
md : d % (t + 1) = d
⊢ a = b ∧ c = d