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. ■