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

Arguments

DOIAuthorDate
MTH.R-2026-6501Adhishraya Sharma2026-09-27T17:43:43Z
DOIMTH.C-2026-6501
Cite

Verification

Library
Submission
Statement digest
7e9cb7f93c34
First verified
2026-09-27T17:43:43Z