Formal target: Corpus.OEIS176477.conjecture1

Each term $a(n)$ is a positive integer.

Exact formal statement

∀ (n : Nat), LE.le.{0} 1 n → And (Eq.{1} (Corpus.OEIS176477.a n).den 1) (LT.lt.{0} 0 (Corpus.OEIS176477.a n))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record