rw [md,hmtl] at hmtr
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
hmtl : (d + (t + 1) * b) % (t + 1) = c
hmtr : (d + (t + 1) * b) % (t + 1) = d % (t + 1)
⊢ 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
hmtl : (d + (t + 1) * b) % (t + 1) = c
hmtr : c = d
⊢ a = b ∧ c = d