Nat.grahamConjecture_of_squarefree

theorem Nat.grahamConjecture_of_squarefree : ∀ {n : ℕ} (f : ℕ → ℕ), (∀ k < n, Squarefree (f k)) → n.GrahamConjecture f

This theorem states a special case of Graham's conjecture, where all the input numbers are squarefree. In particular, for any natural number `n` and any function `f` from natural numbers to natural numbers, if every number less than `n` when passed through `f` yields a squarefree number, then `n` satisfies Graham's Conjecture for function `f`. Here, a number is squarefree if the only squares that can divide it are the squares of units.

More concisely: If every number less than n is squarefree when mapped under a function f, then n satisfies Graham's Conjecture for that function.