Proofgold Proposition

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

type
prop

theory
HotG

name
recip_SNo_invL

proof
PUSRj..

Megalodon
recip_SNo_invL

proofgold address
TMbQ7..^{recip_SNo_invL}

creator
27837 PrQUS../6e3e5..

owner
27837 PrQUS../6e3e5..

term root
85d43..