IMO_2007_Pb_5.lean

import data.pnat.basic
import number_theory.divisors

theorem IMO_2007_Pb_5 (a b: pnat) (h: ↑(4*a*b-1) ∈ (nat.divisors ((4*a^2-1)^2))): a=b :=
begin 
  sorry
end