Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: divides_int x0 x1.

Apply H0 with divides_int x0 (minus_SNo x1).

Assume H1: and (x0 ∈ int) (x1 ∈ int).

Apply H1 with (∃ x2 . and (x2 ∈ int) (mul_SNo x0 x2 = x1)) ⟶ divides_int x0 (minus_SNo x1).

Assume H2: x0 ∈ int.

Assume H3: x1 ∈ int.

Assume H4: ∃ x2 . and (x2 ∈ int) (mul_SNo x0 x2 = x1).

Apply H4 with divides_int x0 (minus_SNo x1).

Let x2 of type ι be given.

Assume H5: (λ x3 . and (x3 ∈ int) (mul_SNo x0 x3 = x1)) x2.

Apply H5 with divides_int x0 (minus_SNo x1).

Assume H6: x2 ∈ int.

Assume H7: mul_SNo x0 x2 = x1.

Apply and3I with x0 ∈ int, minus_SNo x1 ∈ int, ∃ x3 . and (x3 ∈ int) (mul_SNo x0 x3 = minus_SNo x1) leaving 3 subgoals.

The subproof is completed by applying H2.

Apply int_minus_SNo with x1.

The subproof is completed by applying H3.

Let x3 of type ο be given.

Assume H8: ∀ x4 . and (x4 ∈ int) (mul_SNo x0 x4 = minus_SNo x1) ⟶ x3.

Apply H8 with minus_SNo x2.

Apply andI with minus_SNo x2 ∈ int, mul_SNo x0 (minus_SNo x2) = minus_SNo x1 leaving 2 subgoals.

Apply int_minus_SNo with x2.

The subproof is completed by applying H6.

Apply mul_SNo_minus_distrR with x0, x2, λ x4 x5 . x5 = minus_SNo x1 leaving 3 subgoals.

Apply int_SNo with x0.

The subproof is completed by applying H2.

Apply int_SNo with x2.

The subproof is completed by applying H6.

set y4 to be minus_SNo (mul_SNo x0 x2)

set y5 to be minus_SNo x2

Claim L9: ∀ x6 : ι → ο . x6 y5 ⟶ x6 y4

Let x6 of type ι → ο be given.

Assume H9: x6 (minus_SNo x3).

set y7 to be λ x7 . x6

Apply H7 with λ x8 x9 . y7 (minus_SNo x8) (minus_SNo x9).

The subproof is completed by applying H9.

Let x6 of type ι → ι → ο be given.

Apply L9 with λ x7 . x6 x7 y5 ⟶ x6 y5 x7.

Assume H10: x6 y5 y5.

The subproof is completed by applying H10.

■

Proofgold Proof