Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: RealsStruct x0.
Apply RealsStruct_Z_props with x0, RealsStruct_Z x0field0 x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H1: ∀ x1 . x1RealsStruct_Npos x0Field_minus (Field_of_RealsStruct x0) x1RealsStruct_Z x0.
Assume H2: field4 x0RealsStruct_Z x0.
Assume H3: RealsStruct_Npos x0RealsStruct_Z x0.
Assume H4: RealsStruct_Z x0field0 x0.
Assume H5: ∀ x1 . x1RealsStruct_Z x0∀ x2 : ο . (Field_minus (Field_of_RealsStruct x0) x1RealsStruct_Npos x0x2)(x1 = field4 x0x2)(x1RealsStruct_Npos x0x2)x2.
Assume H6: RealsStruct_one x0RealsStruct_Z x0.
Assume H8: ∀ x1 . x1RealsStruct_Z x0Field_minus (Field_of_RealsStruct x0) x1RealsStruct_Z x0.
Assume H9: ∀ x1 . x1RealsStruct_Z x0∀ x2 . x2RealsStruct_Z x0field1b x0 x1 x2RealsStruct_Z x0.
Assume H10: ∀ x1 . x1RealsStruct_Z x0∀ x2 . x2RealsStruct_Z x0field2b x0 x1 x2RealsStruct_Z x0.
The subproof is completed by applying H4.