Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ι → ι be given.
Let x3 of type ι → ι → ι be given.
Apply explicit_Ring_E with
x0,
x1,
x2,
x3,
∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x2 x4 x6 = x2 x5 x6 ⟶ x4 = x5.
Assume H1: ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x2 x4 x5 ∈ x0.
Assume H2: ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x2 x4 (x2 x5 x6) = x2 (x2 x4 x5) x6.
Assume H3: ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x2 x4 x5 = x2 x5 x4.
Assume H4: x1 ∈ x0.
Assume H5: ∀ x4 . x4 ∈ x0 ⟶ x2 x1 x4 = x4.
Assume H6:
∀ x4 . x4 ∈ x0 ⟶ ∃ x5 . and (x5 ∈ x0) (x2 x4 x5 = x1).
Assume H7: ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x3 x4 x5 ∈ x0.
Assume H8: ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x3 x4 (x3 x5 x6) = x3 (x3 x4 x5) x6.
Assume H9: ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x3 x4 (x2 x5 x6) = x2 (x3 x4 x5) (x3 x4 x6).
Assume H10: ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x3 (x2 x4 x5) x6 = x2 (x3 x4 x6) (x3 x5 x6).
Let x4 of type ι be given.
Assume H11: x4 ∈ x0.
Let x5 of type ι be given.
Assume H12: x5 ∈ x0.
Let x6 of type ι be given.
Assume H13: x6 ∈ x0.
Assume H14: x2 x4 x6 = x2 x5 x6.
Apply explicit_Ring_plus_cancelL with
x0,
x1,
x2,
x3,
x6,
x4,
x5 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H13.
The subproof is completed by applying H11.
The subproof is completed by applying H12.
Apply H3 with
x6,
x4,
λ x7 x8 . x8 = x2 x6 x5 leaving 3 subgoals.
The subproof is completed by applying H13.
The subproof is completed by applying H11.
Apply H14 with
λ x7 x8 . x8 = x2 x6 x5.
Apply H3 with
x5,
x6 leaving 2 subgoals.
The subproof is completed by applying H12.
The subproof is completed by applying H13.