Declsecond_probeAxiomsfree
(n : Nat) → @Eq Nat (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) n 0) nOpen
| DOI | Decl | Accession kind | Date |
|---|---|---|---|
| MTH.C-2026-6502 | third_probe | Claim | 2026-09-29T21:58:45Z |
| MTH.R-2026-6502 | third_probe | Argument | 2026-09-29T21:58:45Z |
| MTH.C-2026-6501 | second_probe | Claim | 2026-09-27T17:43:43Z |
| MTH.R-2026-6501 | second_probe | Argument | 2026-09-27T17:43:43Z |
(n : Nat) → @Eq Nat (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) n 0) nOpen
(n m : Nat) →
@Eq Nat (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) n m)
(@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) m n)Open