obtain rfl : a = 1 := h'.symm
case intro.intro.inl.inr
a c₁ d₁ : ℕ
h' : Coprime a 0
h : a * (0 * d₁) = 0 * (a * c₁)
H : a * 0 = 0
⊢ ∃ m, a * c₁ = m * a ∧ 0 * d₁ = m * 0
case intro.intro.inl.inr
c₁ d₁ : ℕ
h' : Coprime 1 0
h : 1 * (0 * d₁) = 0 * (1 * c₁)
H : 1 * 0 = 0
⊢ ∃ m, 1 * c₁ = m * 1 ∧ 0 * d₁ = m * 0