Proofgold Proof

pf
Let x0 of type ι be given. Assume H0: RealsStruct x0. Let x1 of type ι be given. Assume H1: x1 ∈ field0 x0. Assume H2: RealsStruct_leq x0 (field4 x0) x1. Apply If_i_1 with RealsStruct_leq x0 (field4 x0) x1, x1, Field_minus (Field_of_RealsStruct x0) x1. The subproof is completed by applying H2. ■