Proofgold Proposition

∀ x0 . x0 ∈ real ⟶ SNoLt 0 x0 ⟶ ∃ x1 . and (x1 ∈ real) (mul_SNo x0 x1 = 1)

type
prop

theory
HotG

name
pos_real_recip_ex

proof
PUK8p..

Megalodon
pos_real_recip_ex

proofgold address
TMHFw..^{pos_real_recip_ex}

creator
12486 PrGxv../8803e..

owner
12486 PrGxv../8803e..

term root
141e4..