Search for blocks/addresses/...

Proofgold Proof

pf
The subproof is completed by applying Sep_Subq with real, λ x0 . ∃ x1 . and (x1int) (∃ x2 . and (x2setminus omega (Sing 0)) (x0 = div_SNo x1 x2)).