Proofgold Proposition

∀ x0 . SNo x0 ⟶ SNoLt 0 x0 ⟶ and (SNo (recip_SNo_pos x0)) (mul_SNo x0 (recip_SNo_pos x0) = 1)

type
prop

theory
HotG

name
recip_SNo_pos_prop1

proof
PUedh..

Megalodon
recip_SNo_pos_prop1

proofgold address
TMPM3..^{recip_SNo_pos_prop1}

creator
27822 PrQUS../0c52f..

owner
27822 PrQUS../0c52f..

term root
42138..