Proofgold Proposition

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

type
prop

theory
HotG

name
mul_SNo_nonpos_neg

proof
PUewm..

Megalodon
mul_SNo_nonpos_neg

proofgold address
TMHSp..^{mul_SNo_nonpos_neg}

creator
27779 PrQUS../c4d38..

owner
27779 PrQUS../c4d38..

term root
54e1f..