convert dvd_add hkdvdleft hkdvdright using 1
case H.ha
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ 2 * u
case h.e'_4
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ 2 * u = u - 3 * v + (u + 3 * v)