Proofgold Proposition

∀ x0 . nat_p x0 ⟶ add_SNo (minus_SNo 1) (ordsucc x0) = x0

type
prop

theory
HotG

name
add_minus_1_ordsucc

proof
PUY2k..

Megalodon
add_minus_1_ordsucc

proofgold address
TMZCo..^{add_minus_1_ordsucc}

creator
16784 PrGxv../41f5f..

owner
16784 PrGxv../41f5f..

term root
4068c..