import FormalConjectures.ErdosProblems.«890» import TaskSupport namespace Bounty theorem target : fcTypeOfName% "Erdos890.erdos_890.parts.a" := by sorry end Bounty