Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: RealsStruct x0.
Apply RealsStruct_Npos_props with x0, RealsStruct_one x0RealsStruct_Npos x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H1: RealsStruct_Npos x0field0 x0.
Assume H2: explicit_Nats (RealsStruct_Npos x0) (RealsStruct_one x0) (λ x1 . field1b x0 x1 (RealsStruct_one x0)).
Assume H3: RealsStruct_one x0RealsStruct_Npos x0.
Assume H4: ∀ x1 . x1RealsStruct_Npos x0field1b x0 x1 (RealsStruct_one x0) = RealsStruct_one x0∀ x2 : ο . x2.
Assume H5: ∀ x1 . x1RealsStruct_Npos x0∀ x2 : ι → ο . x2 (RealsStruct_one x0)(∀ x3 . x3RealsStruct_Npos x0x2 (field1b x0 x3 (RealsStruct_one x0)))x2 x1.
Assume H6: ∀ x1 . x1RealsStruct_Npos x0∀ x2 . x2RealsStruct_Npos x0explicit_Nats_one_plus (RealsStruct_Npos x0) (RealsStruct_one x0) (λ x3 . field1b x0 x3 (RealsStruct_one x0)) x1 x2 = field1b x0 x1 x2.
Assume H7: ∀ x1 . x1RealsStruct_Npos x0∀ x2 . x2RealsStruct_Npos x0explicit_Nats_one_mult (RealsStruct_Npos x0) (RealsStruct_one x0) (λ x3 . field1b x0 x3 (RealsStruct_one x0)) x1 x2 = field2b x0 x1 x2.
Assume H8: ∀ x1 . x1RealsStruct_Npos x0∀ x2 . x2RealsStruct_Npos x0field1b x0 x1 x2RealsStruct_Npos x0.
Assume H9: ∀ x1 . x1RealsStruct_Npos x0∀ x2 . x2RealsStruct_Npos x0field2b x0 x1 x2RealsStruct_Npos x0.
The subproof is completed by applying H3.