Proofgold Proposition

∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNoLe 0 x0 ⟶ SNoLe x0 x1 ⟶ SNoLe (sqrt_SNo_nonneg x0) (sqrt_SNo_nonneg x1)

type
prop

theory
HotG

name
sqrt_SNo_nonneg_mon

proof
PURry..

Megalodon
sqrt_SNo_nonneg_mon

proofgold address
TMXbf..^{sqrt_SNo_nonneg_mon}

creator
28463 PrQUS../8f32e..

owner
28463 PrQUS../8f32e..

term root
317df..