Proofgold Proposition

∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNoLe 0 x0 ⟶ SNoLe 0 x1 ⟶ mul_SNo x0 x0 = mul_SNo x1 x1 ⟶ x0 = x1

type
prop

theory
HotG

name
SNo_nonneg_sqr_uniq

proof
PUewm..

Megalodon
SNo_nonneg_sqr_uniq

proofgold address
TMa5b..^{SNo_nonneg_sqr_uniq}

creator
27779 PrQUS../705fa..

owner
27779 PrQUS../705fa..

term root
68d62..