Correctness over a domain ·2026-06-21 00:00 UTC
Every successor of a natural number is positive
Enuntiatio — the claim
Every successor of a natural number is positive
Refuted by a natural n with n + 1 ≤ 0
Expressio — the formal statement
import Mathlib.Tactic
theorem succ_pos (n : Nat) : 0 < n + 1Demonstratio — the kernel-checked proof
by omega Q.E.D.
kernel verified: true