cases ht with
| inl h => exact h
| inr h => contradiction
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : a = b ∨ t + 1 = 0
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (d + (t + 1) * b) % (t + 1) = c
hmtr : c = d
⊢ a = b
no goals