Proofgold Proposition

∀ x0 . nat_p x0 ⟶ not (atleastp (ordsucc x0) x0)

type
prop

theory
HotG

name
-

proof
PUNUU..

Megalodon
Pigeonhole_not_atleastp_ordsucc

proofgold address
TMcAU..^{Pigeonhole_not_atleastp_ordsucc}

creator
14937 Pr4zB../bb054..

owner
14937 Pr4zB../bb054..

term root
8a6bd..