Proofgold Proposition

∀ x0 . SNo x0 ⟶ SNoLe 0 x0 ⟶ SNoCutP (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 0)) (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 1)) ⟶ (∀ x1 . x1 ∈ famunion omega (λ x2 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x2) 1) ⟶ ∀ x2 : ο . (SNo x1 ⟶ SNoLe 0 x1 ⟶ SNoLt x0 (mul_SNo x1 x1) ⟶ x2) ⟶ x2) ⟶ SNoLe 0 (SNoCut (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 0)) (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 1)))

type
prop

theory
HotG

name
sqrt_SNo_nonneg_prop1c

proof
PUgxt..

Megalodon
sqrt_SNo_nonneg_prop1c

proofgold address
TMamz..^{sqrt_SNo_nonneg_prop1c}

creator
27854 PrQUS../98e8e..

owner
27854 PrQUS../98e8e..

term root
afcc0..