Proofgold Proposition

∀ x0 . SNo x0 ⟶ SNoLe 0 x0 ⟶ sqrt_SNo_nonneg (exp_SNo_nat x0 2) = x0

type
prop

theory
HotG

name
sqrt_SNo_nonneg_sqr_id

proof
PURry..

Megalodon
sqrt_SNo_nonneg_sqr_id

proofgold address
TMSbG..^{sqrt_SNo_nonneg_sqr_id}

creator
28463 PrQUS../74836..

owner
28463 PrQUS../74836..

term root
4482a..