Probe child
ProvedzzProbeChildARetired. This was a private, throw-away probe used to isolate a verification-harness failure on theorems whose preamble contains a local def; it has no mathematical content and no replacement node.
Preamble
import Mathlib
Formal statement
theorem zzProbeChildA (n m : ℕ) : n + m = n + m := by sorry