Proofgold Proof

pf
Let x0 of type ι be given. Let x1 of type ι be given. Assume H0: x0 ∈ real. Assume H1: SNoLt 0 x0. Assume H2: SNo x0. Assume H3: x1 ∈ omega. Assume H4: eps_ x1 ∈ real. Assume H5: SNoLt 0 (mul_SNo (eps_ x1) x0). Apply pos_real_recip_ex with x0 leaving 2 subgoals. The subproof is completed by applying H0. The subproof is completed by applying H1. ■