Proofgold Term Root Disambiguation

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

as obj
-

as prop
f4ed2..^{Conj_pos_real_recip_ex__2__4}

theory
HotG

stx
b740c..

address
TMHMv..^{Conj_pos_real_recip_ex__2__4}