Proofgold Proposition

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

type
prop

theory
HotG

name
sqrt_SNo_nonneg_mon_strict

proof
PURry..

Megalodon
sqrt_SNo_nonneg_mon_strict

proofgold address
TMMJ2..^{sqrt_SNo_nonneg_mon_strict}

creator
28463 PrQUS../2d28c..

owner
28463 PrQUS../2d28c..

term root
544c3..