import Mathlib.Tactic /-! # International Mathematical Olympiad 2001, Problem 6 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. -/ namespace Imo2001P6 theorem imo2001_p6 {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) := sorry

This problem has a complete solution written by Sara Díaz Real.

The solution was imported from mathlib4/Archive/Imo/Imo2001Q6.lean.