Proofgold Proposition

∀ x0 x1 x2 x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x1 ⟶ SNoLt 0 (add_SNo x3 x4) ⟶ div_SNo (add_SNo x2 (mul_SNo x3 x4)) (add_SNo x3 x4) ∈ SNo_sqrtauxset x0 x1 x2

type
prop

theory
HotG

name
SNo_sqrtauxset_I

proof
PUewm..

Megalodon
SNo_sqrtauxset_I

proofgold address
TMJxC..^{SNo_sqrtauxset_I}

creator
27779 PrQUS../17601..

owner
27779 PrQUS../17601..

term root
4b16a..