rw [h2] at notdvd_2_2
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
not_3_dvd_2 : ¬3 ∣ u - 3 * v
h2 : u - 3 * v = 0
⊢ False
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ 0
not_3_dvd_2 : ¬3 ∣ u - 3 * v
h2 : u - 3 * v = 0
⊢ False