Proofgold Object

λ x0 x1 x2 . famunion x0 (λ x3 . {div_SNo (add_SNo x2 (mul_SNo x3 x4)) (add_SNo x3 x4)|x4 ∈ x1,SNoLt 0 (add_SNo x3 x4)})

type
ι → ι → ι → ι

theory
HotG

name
SNo_sqrtauxset

definition
PUewm..

Megalodon
SNo_sqrtauxset

proofgold address
TMHDv..^{SNo_sqrtauxset}

creator
27779 PrQUS../8eaff..

owner
27779 PrQUS../8eaff..

term root
211c6..