Proofgold Proposition

∀ x0 . SNo x0 ⟶ (x0 = 0 ⟶ ∀ x1 : ο . x1) ⟶ mul_SNo x0 (recip_SNo x0) = 1

type
prop

theory
HotG

name
recip_SNo_invR

proof
PUSRj..

Megalodon
recip_SNo_invR

proofgold address
TMRSb..^{recip_SNo_invR}

creator
27837 PrQUS../dbcaa..

owner
27837 PrQUS../dbcaa..

term root
33c26..