IMO 2001 Q6

Let $a$, $b$, $c$, $d$ be integers with $a > b > c > d > 0$. Suppose that

$$ ac + bd = (a + b - c + d) * (-a + b + c + d). $$

Prove that $ab + cd$ is not prime.

theorem imo2001_q6 {a : ℤ} {b : ℤ} {c : ℤ} {d : ℤ} (hd : 0 < d) (hdc : d < c) (hcb : c < b) (hba : b < a) (h : a * c + b * d = (a + b - c + d) * (-a + b + c + d)) : ¬Prime (a * b + c * d)