Formal target: Corpus.OEIS53000.conjecture

Conjecture: $a(n) \le 1 + \phi(n)$ for $n > 0$.

Exact formal statement

∀ (n : Nat), LT.lt.{0} 0 n → LE.le.{0} (Corpus.OEIS53000.a n) (HAdd.hAdd.{0, 0, 0} 1 n.totient)

This target is a formal statement, not a proof of the problem.

Environment availability: available.