IMO 2001 Q6

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

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

Prove that $a*b + c*d$ is not prime.

theorem imo2001_q6 {a b c d : Int} (hd : LT.lt 0 d) (hdc : LT.lt d c) (hcb : LT.lt c b) (hba : LT.lt b a) (h : Eq (HAdd.hAdd (HMul.hMul a c) (HMul.hMul b d)) (HMul.hMul (HAdd.hAdd (HSub.hSub (HAdd.hAdd a b) c) d) (HAdd.hAdd (HAdd.hAdd (HAdd.hAdd (Neg.neg a) b) c) d))) : Not (Prime (HAdd.hAdd (HMul.hMul a b) (HMul.hMul c d)))