Proofgold Object

λ x0 x1 x2 . ∃ x3 . and (x3 ∈ RealsStruct_Npos x0) (field2b x0 x1 x3 = x2)

type
ι → ι → ι → ο

theory
HotG

name
RealsStruct_divides

definition
PUVyd..

Megalodon
RealsStruct_divides

proofgold address
TMEjv..^{RealsStruct_divides}

creator
5857 Pr6Pc../14b71..

owner
5857 Pr6Pc../14b71..

term root
9b1a1..