Proofgold Term Root Disambiguation

∀ x0 . x0 ∈ setminus omega (Sing 0) ⟶ ∀ x1 . nat_p x1 ⟶ ∃ x2 . and (x2 ∈ omega) (∃ x4 . and (x4 ∈ x0) (x1 = add_nat (mul_nat x2 x0) x4))

as obj
-

as prop
b1d85..^{quotient_remainder_nat}

theory
HotG

stx
e9e67..

address
TMbet..^{quotient_remainder_nat}