Proofgold Proposition

∀ x0 . nat_p x0 ⟶ ordsucc x0 ∈ mul_nat 2 (ordsucc x0)

type
prop

theory
HotG

name
ordsucc_in_double_nat_ordsucc

proof
PUWsr..

Megalodon
ordsucc_in_double_nat_ordsucc

proofgold address
TMdAc..^{ordsucc_in_double_nat_ordsucc}

creator
23950 Pr5Zc../567dd..

owner
23950 Pr5Zc../567dd..

term root
34a6c..