Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: RealsStruct x0.
Apply explicit_OrderedField_sum_squares_zero_inv with field0 x0, field4 x0, RealsStruct_one x0, field1b x0, field2b x0, RealsStruct_leq x0.
Apply explicit_OrderedField_of_RealsStruct with x0.
The subproof is completed by applying H0.