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