linear_combination over ℤ: never divide (h/2 is integer division)

In linear_combination h' / 2 over ℤ, / is Int division, so ring fails with a goal containing x / 2 terms. Instead prove the doubled equation and cancel: mul_left_cancel₀ (two_ne_zero (α := ℤ)) (by linear_combination h'). For olympiad Diophantine back-substitution (y - 1 = t*m, plug into y² = ...), compute the coefficient by hand. If y = tm + 1, the difference is (2j+1)² - (tm+1)² = (2j - tm)(2j + tm + 2), so linear_combination h' + (2*j + t*m + 2) * hm proves t * (...) = 0; then (mul_eq_zero.1 _).resolve_left. Also, ring happily normalizes 2^(2*(k+1)+1) = 8*(2^k)^2 with a symbolic k, and IsCoprime.pow_left ⟨-i, 1, by ring⟩ gives IsCoprime (2^k) (2*i+1) in one line.