Proofgold Term Root Disambiguation

∀ x0 x1 . 1 ∈ x0 ⟶ divides_nat x0 x1 ⟶ not (divides_nat x0 (ordsucc x1))

as obj
-

as prop
8d635..^{nat_1In_not_divides_ordsucc}

theory
HotG

stx
00571..

address
TMMcd..^{nat_1In_not_divides_ordsucc}