obtain ⟨y, hy⟩ := h2
case intro
n a b c d : ℤ
h2 : c ≡ d [ZMOD n]
x : ℤ
hx : a - b = n * x
⊢ a + c ≡ b + d [ZMOD n]
case intro.intro
n a b c d x : ℤ
hx : a - b = n * x
y : ℤ
hy : c - d = n * y
⊢ a + c ≡ b + d [ZMOD n]