Proofgold Proposition

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

type
prop

theory
HotG

name
recip_SNo_pos_invR

proof
PUSRj..

Megalodon
recip_SNo_pos_invR

proofgold address
TMYV2..^{recip_SNo_pos_invR}

creator
27837 PrQUS../f5558..

owner
27837 PrQUS../f5558..

term root
12c41..