second deposit, on-demand dispatch

The source behind MTH.C-2026-6501, as deposited.

What the author says it does

A Lean-core theorem with actual content, to exercise dispatch and the export store.

Statement of second_probe, as the kernel has it

(n : Nat) → @Eq Nat (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) n 0) n

Source, as submitted

/-!
# Mathesis deposit

@kind: result
@title: second deposit, on-demand dispatch
@module: Submission
@decls: second_probe
@pin: leanprover/lean4:v4.31.0

@gloss:
  A Lean-core theorem with actual content, to exercise dispatch and the export store.
-/

theorem second_probe (n : Nat) : n + 0 = n := Nat.add_zero n